paulson [Thu, 20 Dec 2001 15:20:07 +0100] rev 12561
new hfootref macro for Web links
paulson [Thu, 20 Dec 2001 15:17:48 +0100] rev 12560
converted some ZF/Induct examples to Isar
berghofe [Thu, 20 Dec 2001 15:00:02 +0100] rev 12559
cast_ok and match_exception_entry no longer disabled (thanks to
improvement of code generator).
berghofe [Thu, 20 Dec 2001 14:59:09 +0100] rev 12558
cast_ok no longer disabled (thanks to improvement of code generator).
berghofe [Thu, 20 Dec 2001 14:58:18 +0100] rev 12557
Implemented higher order modes.
berghofe [Thu, 20 Dec 2001 14:57:54 +0100] rev 12556
Moved "code" attribute to Pure/codegen.ML
berghofe [Thu, 20 Dec 2001 14:57:15 +0100] rev 12555
"code" attribute is now managed by basic code generator module.
berghofe [Thu, 20 Dec 2001 14:55:28 +0100] rev 12554
Declared characteristic equations for < on nat for code generation.