src/HOL/IsaMakefile
2008-11-29 nipkow 2008-11-29 new file float_syntax.ML
2008-11-17 wenzelm 2008-11-17 removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-15 wenzelm 2008-11-15 clean: added HOL-Main;
2008-11-13 haftmann 2008-11-13 moved assert to Heap_Monad.thy
2008-10-21 berghofe 2008-10-21 Added nominal_inductive2.ML
2008-10-17 wenzelm 2008-10-17 reactivated HOL-Matrix; minor cleanup;
2008-10-16 ballarin 2008-10-16 Removed ex/Locales.thy.
2008-10-14 wenzelm 2008-10-14 renamed AtpThread to AtpWrapper;
2008-10-04 wenzelm 2008-10-04 replaced ISATOOL by ISABELLE_TOOL;
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);
2008-10-03 wenzelm 2008-10-03 removed old/unused setup of raw ATP oracles;
2008-09-29 haftmann 2008-09-29 separate HOL-Main image
2008-09-28 wenzelm 2008-09-28 HOL no longer depends on HOL-Plain;
2008-09-27 wenzelm 2008-09-27 HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
2008-09-22 berghofe 2008-09-22 Added coherent logic prover.
2008-09-22 haftmann 2008-09-22 different session branches for HOL-Plain vs. Plain
2008-09-16 haftmann 2008-09-16 moved term_of syntax to separate theory
2008-09-16 haftmann 2008-09-16 generic value command
2008-09-03 nipkow 2008-09-03 removed ex/Puzzle
2008-09-02 nipkow 2008-09-02 Replaced Library/NatPair by Nat_Int_Bij.
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-08-27 haftmann 2008-08-27 added HOL/ex/Numeral.thy
2008-08-05 krauss 2008-08-05 fix HOL/ex/LexOrds.thy; add to regression
2008-08-01 ballarin 2008-08-01 Generalised polynomial lemmas from cring to ring.
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ballarin 2008-07-29 New theory on divisibility; Restructured presentation.
2008-07-29 haftmann 2008-07-29 corrected Pure dependency
2008-07-25 haftmann 2008-07-25 tuned
2008-07-21 haftmann 2008-07-21 (adjusted)
2008-07-16 berghofe 2008-07-16 Added Standardization theory to nominal examples.
2008-07-04 haftmann 2008-07-04 added marginal setup for code generation
2008-07-03 wenzelm 2008-07-03 removed old Complex/ex/NSPrimes.thy;
2008-07-03 wenzelm 2008-07-03 more precise dependencies for HOL-Word and HOL-NSA;
2008-07-03 huffman 2008-07-03 add HOL-NSA
2008-07-03 haftmann 2008-07-03 code antiquotation roaring ahead
2008-07-02 haftmann 2008-07-02 code antiquotation roaring ahead
2008-07-01 wenzelm 2008-07-01 clean: HOL-Plain;
2008-07-01 haftmann 2008-07-01 (removed Complex/ROOT.ML)
2008-07-01 haftmann 2008-07-01 HOL += HOL-Complex
2008-06-30 haftmann 2008-06-30 HOL-Complex with proof terms
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-23 wenzelm 2008-06-23 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
2008-06-20 haftmann 2008-06-20 moved Float.thy to Library
2008-06-12 wenzelm 2008-06-12 some reformatting;
2008-06-12 urbanc 2008-06-12 added CK_Machine to the nominal section
2008-06-10 wenzelm 2008-06-10 added HOL/Tools/induct_tacs.ML;
2008-06-10 haftmann 2008-06-10 major refactorings in code generator modules
2008-06-01 urbanc 2008-06-01 new example
2008-05-13 krauss 2008-05-13 fixed makefile
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-22 haftmann 2008-04-22 dropped theory PreList
2008-04-22 haftmann 2008-04-22 added theory Sublist_Order
2008-04-16 wenzelm 2008-04-16 removed unused TLA/Memory/MIParameters.thy;
2008-04-08 krauss 2008-04-08 fixed makefiles
2008-03-20 haftmann 2008-03-20 added theory Library/Enum.thy
2008-03-14 nipkow 2008-03-14 Added lemmas
2008-03-12 haftmann 2008-03-12 separated Random.thy from Quickcheck.thy
2008-03-07 haftmann 2008-03-07 canonical order on option type
2008-03-04 urbanc 2008-03-04 added new example
2008-03-03 krauss 2008-03-03 new theory of red-black trees, an efficient implementation of finite maps.