Welcome to the HOL-CASL home page!
This work is a part of the Common
What is HOL-CASL?
HOL-CASL is a theorem proving system for CASL.
It is based on the generic theorem prover Isabelle.
HOL-CASL uses the CASL tool set (CATS)
to analyse and encode a CASL library.
New features of release 0.85:
free (=inductively defined) predicates are supported.
partial constructors in generated types are supported.
- default simplifier set has been improved.
- better library management.
part of the basic datatypes have been verified within HOL-CASL!
See the CoFI
tools home page.
Different colleagues from CoFI have participated through various discussions
to this work. They deserve our warmest thanks.