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.
ftp://ftp.cl.cam.ac.uk/ml/92.tar.Z
Comments, Experience, Additions
Next Language: ISBL