src/HOL/IsaMakefile
2002-05-15 nipkow 2002-05-15 Divides.ML -> Divides_lemmas.ML Converted Divides.thy to Isar.
2002-05-10 nipkow 2002-05-10 *** empty log message ***
2002-05-10 nipkow 2002-05-10 added dep on IMP/Compiler0
2002-05-08 paulson 2002-05-08 some ex files converted to Isar
2002-04-04 paulson 2002-04-04 conversion of Induct/{Slist,Sexp} to Isar scripts
2002-04-02 paulson 2002-04-02 conversion of some HOL/Induct proof scripts to Isar
2002-03-14 paulson 2002-03-14 removed ex/set.ML
2002-03-06 wenzelm 2002-03-06 tuned;
2002-03-06 wenzelm 2002-03-06 added HOL-Hyperreal-ex;
2002-03-05 prensani 2002-03-05 Target HoareParallel in IsaMakefile
2002-03-02 wenzelm 2002-03-02 temporarily disabled HoareParallel target;
2002-03-01 prensani 2002-03-01 Completed annonce of HoareParallel
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-26 wenzelm 2002-02-26 Isar_examples/W_correct moved to W0;
2002-02-21 wenzelm 2002-02-21 theory Option has been assimilated by Datatype;
2002-02-21 kleing 2002-02-21 new MicroJava document
2002-02-16 wenzelm 2002-02-16 converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;
2002-01-28 schirmer 2002-01-28 Bali added
2002-01-18 wenzelm 2002-01-18 fixed document setup of HOL-Library;
2002-01-17 nipkow 2002-01-17 Lex dependencies modified
2002-01-13 wenzelm 2002-01-13 added HOL/Real/document/root.tex;
2002-01-13 wenzelm 2002-01-13 Real/Complex_Numbers.thy;
2002-01-09 wenzelm 2002-01-09 converted theory Transitive_Closure;
2002-01-08 wenzelm 2002-01-08 HOL-Hyperreal produces an image (again);
2001-12-19 wenzelm 2001-12-19 HOL/IMP: include session graph;
2001-12-16 kleing 2001-12-16 MicroJava exception merge
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