C A T
CAT is a Computer Arithmetic Toolkit for
the Isabelle/HOL theorem prover. It provides a theory for integers,
a rewrite engine for integer expressions, and a decision procedure
for Presburger formulas.
Version 1.0 beta of CAT is available here which requires Isabelle94-8
and Poly ML 3.2.
- Source code distribution: CAT.tgz
(136 kByte)
- Documentation (also included in the distribution):
CAT.ps.gz (85 kByte)
This page was last updated
on 25th April 2001.