src/HOL/IsaMakefile
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.
2008-02-27 haftmann 2008-02-27 added theories for imperative HOL
2008-02-27 chaieb 2008-02-27 HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
2008-02-25 chaieb 2008-02-25 Added dependency of Library on Pocklington.thy
2008-02-25 chaieb 2008-02-25 Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
2008-02-20 wenzelm 2008-02-20 removed ex/NBE.thy;
2008-01-25 haftmann 2008-01-25 distinguished examples for Efficient_Nat.thy
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-02 haftmann 2008-01-02 improved evaluation mechanism
2007-12-20 wenzelm 2007-12-20 moved Pure/General/random_word.ML to Tools/random_word.ML;
2007-12-20 wenzelm 2007-12-20 updated HOL-Nominal-Examples deps;
2007-12-11 haftmann 2007-12-11 joined EvenOdd theory with Parity
2007-12-07 krauss 2007-12-07 Adding "ex/Induction_Scheme.thy" to tests
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-12-05 haftmann 2007-12-05 dropped Classpackage.thy
2007-11-13 berghofe 2007-11-13 Added new program extraction examples.
2007-11-06 wenzelm 2007-11-06 activated HOL-SizeChange; tuned;
2007-11-06 wenzelm 2007-11-06 removed dependencies on Size_Change_Termination from HOL-Library;
2007-11-06 krauss 2007-11-06 moved stuff about size change termination to its own session
2007-11-05 kleing 2007-11-05 add root.bib for Word document
2007-10-24 wenzelm 2007-10-24 fixed HOL-Statespace for case-sensitive file-system;
2007-10-24 schirmer 2007-10-24 added Statespace library
2007-10-12 haftmann 2007-10-12 consolidated naming conventions for code generator theories
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
2007-10-08 urbanc 2007-10-08 changed VC-Compatible to VC_Compatible
2007-10-08 urbanc 2007-10-08 added the two new examples from Nominal to the build process
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-29 kleing 2007-09-29 Added target for proof term sessions (those that need -p 2)
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-18 wenzelm 2007-09-18 moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML