src/HOL/IsaMakefile
2001-12-10 berghofe 2001-12-10 Added new files (code generator and examples).
2001-12-09 kleing 2001-12-09 HOL/IMP converted to Isar
2001-12-06 wenzelm 2001-12-06 include session graph;
2001-12-06 wenzelm 2001-12-06 renamed theory Finite to Finite_Set and converted;
2001-12-04 wenzelm 2001-12-04 added Higher_Order_Logic.thy;
2001-11-21 wenzelm 2001-11-21 theory Inverse_Image converted and moved to Set;
2001-11-20 wenzelm 2001-11-20 tuned;
2001-11-16 paulson 2001-11-16 even more theories from Jacques
2001-11-15 paulson 2001-11-15 new theories from Jacques Fleuriot
2001-11-08 wenzelm 2001-11-08 ex/document/root.bib;
2001-11-06 wenzelm 2001-11-06 renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy; added ex/Locales.thy;
2001-11-05 paulson 2001-11-05 new Sqrt example
2001-11-03 wenzelm 2001-11-03 moved String into Main;
2001-11-02 wenzelm 2001-11-02 theory Calculation move to Set;
2001-10-20 wenzelm 2001-10-20 document graphs for several sessions;
2001-10-19 wenzelm 2001-10-19 got rid of Provers/split_paired_all.ML;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 removed Ord.thy (now part of HOL.thy).
2001-10-04 wenzelm 2001-10-04 $(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
2001-10-03 wenzelm 2001-10-03 Tools/induct_attrib.ML now part of Pure;
2001-10-01 wenzelm 2001-10-01 added Ordinals example;
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2001-09-27 wenzelm 2001-09-27 updated;
2001-09-27 wenzelm 2001-09-27 ex/Hilbert_Classical.thy ex/document/root.tex;
2001-09-01 wenzelm 2001-09-01 HOL-Real-Hyperreal made a plain session (no longer an image);
2001-08-31 berghofe 2001-08-31 Added new files for code generator.
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-23 paulson 2001-07-23 new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-03 wenzelm 2001-07-03 Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential uses of this ML file (HOL/Library is in the default load path);
2001-07-03 paulson 2001-07-03 Locale-based group theory proofs
2001-06-16 oheimb 2001-06-16 added NanoJava
2001-06-10 paulson 2001-06-10 new GroupTheory example, e.g. the Sylow theorem (preliminary version)
2001-06-09 paulson 2001-06-09 moved Primes.thy from NumberTheory to Library
2001-06-08 nipkow 2001-06-08 Removed BCV
2001-05-31 wenzelm 2001-05-31 added HOL-CTL;
2001-05-31 oheimb 2001-05-31 added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-08 paulson 2001-05-08 conversion of Auth/TLS to Isar script
2001-04-24 paulson 2001-04-24 (rough) conversion of Auth/Recur to Isar format
2001-04-12 paulson 2001-04-12 converted many HOL/Auth theories to Isar scripts
2001-03-28 nipkow 2001-03-28 MicroJava/BV dependencies incomplete
2001-03-23 nipkow 2001-03-23 added one point simprocs for bounded quantifiers
2001-03-05 paulson 2001-03-05 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-02 paulson 2001-03-02 conversion of Message.thy to Isar format
2001-02-15 oheimb 2001-02-15 Ord.thy/.ML converted to Isar
2001-02-13 paulson 2001-02-13 partial conversion to Isar script style in HOL/Auth removes some .ML files
2001-02-09 kleing 2001-02-09 removed MicroJava/Digest.thy
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2001-02-03 wenzelm 2001-02-03 Induct: converted some theories to new-style format;
2001-02-01 oheimb 2001-02-01 converted to Isar, simplifying recursion on class hierarchy
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2001-01-28 nipkow 2001-01-28 fixed set comprehension print translation
2001-01-26 wenzelm 2001-01-26 tuned;
2001-01-26 wenzelm 2001-01-26 Transitive_Closure turned into new-style theory;
2001-01-23 wenzelm 2001-01-23 added HOL-Unix example;
2001-01-20 wenzelm 2001-01-20 added Library/Ring_and_Field_Example.thy;
2001-01-19 wenzelm 2001-01-19 added HOL/Library/Nested_Environment.thy;
2001-01-16 kleing 2001-01-16 removed obsolete MicroJava/JVM/Store.thy
2001-01-16 wenzelm 2001-01-16 removed ex/StringEx.ML;
2001-01-12 wenzelm 2001-01-12 added Induct/Sigma_Algebra.thy;
2001-01-07 wenzelm 2001-01-07 removed MicroJava/BV/Convert.thy;