isabelle: Changelog

webertj [Wed, 24 Nov 2004 19:51:33 +0100] rev 15329

Removed a "Matches are not exhaustive" warning

nipkow [Wed, 24 Nov 2004 11:13:00 +0100] rev 15328

mod because of change in finite set induction

nipkow [Wed, 24 Nov 2004 11:12:10 +0100] rev 15327

changed the order of !!-quantifiers in finite set induction. In Isar you can now write (insert x F) rather than the counterintuitive (insert F x).

berghofe [Wed, 24 Nov 2004 10:37:38 +0100] rev 15326

Made test_term escape special characters in strings that caused the ML compiler to fail.

berghofe [Wed, 24 Nov 2004 10:32:33 +0100] rev 15325

Functions nat_to_bv and bv_to_nat now really operate on natural numbers.

berghofe [Wed, 24 Nov 2004 10:30:19 +0100] rev 15324

Added EfficientNat

berghofe [Wed, 24 Nov 2004 10:29:44 +0100] rev 15323

Code generator plug-in for implementing natural numbers by integers.

isabelle