src/HOL/IsaMakefile
2008-10-04 ago replaced ISATOOL by ISABELLE_TOOL;
2008-10-03 ago version of sledgehammer using threads instead of processes, misc cleanup;
2008-10-03 ago removed old/unused setup of raw ATP oracles;
2008-09-29 ago separate HOL-Main image
2008-09-28 ago HOL no longer depends on HOL-Plain;
2008-09-27 ago HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
2008-09-22 ago Added coherent logic prover.
2008-09-22 ago different session branches for HOL-Plain vs. Plain
2008-09-16 ago moved term_of syntax to separate theory
2008-09-16 ago generic value command
2008-09-03 ago removed ex/Puzzle
2008-09-02 ago Replaced Library/NatPair by Nat_Int_Bij.
2008-08-28 ago restructured and split code serializer module
2008-08-27 ago added HOL/ex/Numeral.thy
2008-08-05 ago fix HOL/ex/LexOrds.thy; add to regression
2008-08-01 ago Generalised polynomial lemmas from cring to ring.
2008-07-30 ago New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ago New theory on divisibility;
2008-07-29 ago corrected Pure dependency
2008-07-25 ago tuned
2008-07-21 ago (adjusted)
2008-07-16 ago Added Standardization theory to nominal examples.
2008-07-04 ago added marginal setup for code generation
2008-07-03 ago removed old Complex/ex/NSPrimes.thy;
2008-07-03 ago more precise dependencies for HOL-Word and HOL-NSA;
2008-07-03 ago add HOL-NSA
2008-07-03 ago code antiquotation roaring ahead
2008-07-02 ago code antiquotation roaring ahead
2008-07-01 ago clean: HOL-Plain;
2008-07-01 ago (removed Complex/ROOT.ML)
2008-07-01 ago HOL += HOL-Complex
2008-06-30 ago HOL-Complex with proof terms
2008-06-26 ago established Plain theory and image
2008-06-23 ago moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
2008-06-20 ago moved Float.thy to Library
2008-06-12 ago some reformatting;
2008-06-12 ago added CK_Machine to the nominal section
2008-06-10 ago added HOL/Tools/induct_tacs.ML;
2008-06-10 ago major refactorings in code generator modules
2008-06-01 ago new example
2008-05-13 ago fixed makefile
2008-04-25 ago Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-22 ago dropped theory PreList
2008-04-22 ago added theory Sublist_Order
2008-04-16 ago removed unused TLA/Memory/MIParameters.thy;
2008-04-08 ago fixed makefiles
2008-03-20 ago added theory Library/Enum.thy
2008-03-14 ago Added lemmas
2008-03-12 ago separated Random.thy from Quickcheck.thy
2008-03-07 ago canonical order on option type
2008-03-04 ago added new example
2008-03-03 ago new theory of red-black trees, an efficient implementation of finite maps.
2008-02-27 ago added theories for imperative HOL
2008-02-27 ago HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
2008-02-25 ago Added dependency of Library on Pocklington.thy
2008-02-25 ago Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
2008-02-20 ago removed ex/NBE.thy;
2008-01-25 ago distinguished examples for Efficient_Nat.thy
2008-01-15 ago joined theories IntDef, Numeral, IntArith to theory Int
2008-01-02 ago improved evaluation mechanism