src/ZF/IsaMakefile
2008-10-04 ago replaced ISATOOL by ISABELLE_TOOL;
2008-09-19 ago add theory graph to ZF document
2008-06-14 ago removed obsolete ML_SUFFIX;
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments
2007-05-31 ago moved Integ files to canonical place;
2007-04-26 ago removed lagacy ML files;
2005-10-19 ago removed obsolete thy_syntax.ML;
2005-10-11 ago ML_SUFFIX in targets (experimental);
2005-03-28 ago conversion of UNITY to Isar scripts
2004-09-19 ago converting UNITY/MultisetSum.ML to Isar script
2004-09-17 ago converted ZF/Induct/Multiset to Isar script
2004-07-29 ago documents for ZF-AC and ZF-Constructible
2004-06-08 ago Groups, Rings and supporting lemmas
2003-07-09 ago converting more theories to Isar scripts, and tidying
2003-07-08 ago Conversion of ZF/UNITY/{FP,Union} to Isar script.
2003-06-30 ago Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
2003-06-27 ago Conversion of theory UNITY to Isar script
2003-06-27 ago Conversion of AllocBase to new-style
2003-06-26 ago Conversion of "Merge" to Isar format
2003-06-25 ago Conversion of UNITY/Distributor to Isar script. General tidy-up.
2003-06-24 ago Converting ZF/UNITY to Isar
2003-06-20 ago conversion of ClientImpl to Isar script
2003-06-20 ago Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
2003-05-29 ago Introduction of the theories UNITY/Merge, UNITY/ClientImpl
2003-05-28 ago some new ZF/UNITY material from Sidi Ehmety
2003-01-15 ago more new-style theories
2002-10-09 ago Re-organization of Constructible theories
2002-09-21 ago converted to Isar script
2002-09-07 ago conversion of ZF/Integ/{Int,Bin} to Isar scripts
2002-08-28 ago various new lemmas for Constructible
2002-08-24 ago conversion of ZF/IntDiv to Isar script
2002-08-15 ago Relativization and absoluteness for DPow!!
2002-08-13 ago In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
2002-08-13 ago new file Constructible/Satisfies_absolute.thy
2002-07-30 ago removal of twos_compl.ML, which is not really needed
2002-07-28 ago tuned document;
2002-07-14 ago Removal of mono.thy
2002-07-14 ago improved presentation markup
2002-07-10 ago Fixed quantified variable name preservation for ball and bex (bounded quants)
2002-07-09 ago converted List to new-style
2002-07-09 ago new files
2002-07-04 ago Constructible/document/root.tex;
2002-07-02 ago conversion of QPair to Isar
2002-06-29 ago conversion of many files to Isar format
2002-06-23 ago conversion of Sum, pair to Isar script
2002-06-22 ago converted Bool, Trancl, Rel to Isar format
2002-06-19 ago added the Constructible target
2002-06-19 ago conversion of Cardinal to Isar script
2002-06-18 ago conversion of Fixedpt to Isar script
2002-06-16 ago conversion of CardinalArith to Isar script
2002-05-31 ago conversion of Finite to Isar format
2002-05-24 ago converted Update to Isar
2002-05-24 ago conversion of Perm to Isar. Strengthening of comp_fun_apply
2002-05-22 ago conversion of Nat to Isar
2002-05-21 ago conversion of OrdQuant.ML to Isar
2002-05-21 ago converted domrange to Isar and merged with equalities
2002-05-20 ago conversion of equalities and WF to Isar
2002-05-18 ago converted Epsilon to Isar
2002-05-18 ago converted Arith, Univ, func to Isar format!
2002-05-16 ago converting Ordinal.ML to Isar format