Isabelle-92

A generic theorem prover, supporting a wide variety of logics. A system of type classes allows polymorphic object-logics with overloading and automatic type inference.