src/ZF/IsaMakefile
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;
2001-11-07 paulson 2001-11-07 Sidi Ehmety's port of the fold_set operator and multisets to ZF. Also, fixes to the cancellation simprocs and a few new standard lemmas.
2001-11-07 paulson 2001-11-07 reorganization of the ZF examples
2001-08-08 paulson 2001-08-08 new ZF/UNITY theory
2001-07-06 paulson 2001-07-06 two Isar tactic scripts
2001-06-26 paulson 2001-06-26 tidying and consolidating files
2001-02-03 paulson 2001-02-03 commutation theory, ported by Sidi Ehmety
2000-08-18 paulson 2000-08-18 new example ZF/ex/NatSum
2000-08-11 paulson 2000-08-11 new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
2000-08-07 paulson 2000-08-07 instantiated Cancel_Numerals for "nat" in ZF
2000-05-05 wenzelm 2000-05-05 removed Pure/section_utils.ML;
1999-02-03 wenzelm 1999-02-03 usedir -r;
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-09-25 paulson 1998-09-25 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-23 paulson 1998-09-23 New directory Integ for the integers
1998-09-10 paulson 1998-09-10 new file AC/WO1_WO7.thy
1998-07-17 paulson 1998-07-17 added Main and Update
1998-05-01 paulson 1998-05-01 Let.ML and Let.thy had been omitted
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1997-12-19 wenzelm 1997-12-19 log files; 'clean' target;
1997-07-07 wenzelm 1997-07-07 eliminated chmod -w;
1997-05-06 wenzelm 1997-05-06 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
1997-04-25 wenzelm 1997-04-25 removed -c option;
1997-03-20 wenzelm 1997-03-20 isatool usedir;
1997-01-09 wenzelm 1997-01-09 IsaMakefile for ZF;