src/ZF/IsaMakefile
2003-06-27 paulson 2003-06-27 Conversion of theory UNITY to Isar script
2003-06-27 paulson 2003-06-27 Conversion of AllocBase to new-style
2003-06-26 paulson 2003-06-26 Conversion of "Merge" to Isar format
2003-06-25 paulson 2003-06-25 Conversion of UNITY/Distributor to Isar script. General tidy-up.
2003-06-24 paulson 2003-06-24 Converting ZF/UNITY to Isar
2003-06-20 paulson 2003-06-20 conversion of ClientImpl to Isar script
2003-06-20 paulson 2003-06-20 Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
2003-05-29 paulson 2003-05-29 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
2003-05-28 paulson 2003-05-28 some new ZF/UNITY material from Sidi Ehmety
2003-01-15 paulson 2003-01-15 more new-style theories
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-09-21 paulson 2002-09-21 converted to Isar script
2002-09-07 paulson 2002-09-07 conversion of ZF/Integ/{Int,Bin} to Isar scripts
2002-08-28 paulson 2002-08-28 various new lemmas for Constructible
2002-08-24 paulson 2002-08-24 conversion of ZF/IntDiv to Isar script
2002-08-15 paulson 2002-08-15 Relativization and absoluteness for DPow!!
2002-08-13 paulson 2002-08-13 In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy
2002-08-13 paulson 2002-08-13 new file Constructible/Satisfies_absolute.thy
2002-07-30 paulson 2002-07-30 removal of twos_compl.ML, which is not really needed
2002-07-28 wenzelm 2002-07-28 tuned document;
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-10 paulson 2002-07-10 Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.
2002-07-09 paulson 2002-07-09 converted List to new-style
2002-07-09 paulson 2002-07-09 new files
2002-07-04 wenzelm 2002-07-04 Constructible/document/root.tex;
2002-07-02 paulson 2002-07-02 conversion of QPair to Isar
2002-06-29 paulson 2002-06-29 conversion of many files to Isar format
2002-06-23 paulson 2002-06-23 conversion of Sum, pair to Isar script
2002-06-22 paulson 2002-06-22 converted Bool, Trancl, Rel to Isar format
2002-06-19 paulson 2002-06-19 added the Constructible target
2002-06-19 paulson 2002-06-19 conversion of Cardinal to Isar script
2002-06-18 paulson 2002-06-18 conversion of Fixedpt to Isar script
2002-06-16 paulson 2002-06-16 conversion of CardinalArith to Isar script
2002-05-31 paulson 2002-05-31 conversion of Finite to Isar format
2002-05-24 paulson 2002-05-24 converted Update to Isar
2002-05-24 paulson 2002-05-24 conversion of Perm to Isar. Strengthening of comp_fun_apply
2002-05-22 paulson 2002-05-22 conversion of Nat to Isar
2002-05-21 paulson 2002-05-21 conversion of OrdQuant.ML to Isar
2002-05-21 paulson 2002-05-21 converted domrange to Isar and merged with equalities
2002-05-20 paulson 2002-05-20 conversion of equalities and WF to Isar
2002-05-18 paulson 2002-05-18 converted Epsilon to Isar
2002-05-18 paulson 2002-05-18 converted Arith, Univ, func to Isar format!
2002-05-16 paulson 2002-05-16 converting Ordinal.ML to Isar format
2002-05-13 paulson 2002-05-13 converted Order.ML OrderType.ML OrderArith.ML to Isar format
2002-05-10 paulson 2002-05-10 now-obsolete ML files
2002-04-15 paulson 2002-04-15 converted theory ex/Limit to Isar script, but it still needs work!
2002-01-16 paulson 2002-01-16 Isar version of AC
2002-01-08 paulson 2002-01-08 Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style
2001-12-29 wenzelm 2001-12-29 tuned document sources;
2001-12-28 paulson 2001-12-28 conversion to Isar/ZF
2001-12-25 paulson 2001-12-25 conversion to Isar
2001-12-22 paulson 2001-12-22 Resid converted to Isar/ZF
2001-12-20 paulson 2001-12-20 converted some ZF/Induct examples to Isar
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-12-08 wenzelm 2001-12-08 added Main.ML;
2001-11-16 wenzelm 2001-11-16 Ntree and Brouwer converted and moved to ZF/Induct;
2001-11-15 wenzelm 2001-11-15 added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
2001-11-14 wenzelm 2001-11-14 added Induct/Binary_Trees.thy, Induct/Datatypes.thy; removed ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy;
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;