Isabelle is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). See the Isabelle overview.

This site provides general information on Isabelle, more specific information is available from the local sites