2011-12-09 kuncar 2011-12-09 added dependencies
2011-12-04 huffman 2011-12-04 merged
2011-12-04 huffman 2011-12-04 remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
2011-12-04 nipkow 2011-12-04 missing dependency
2011-12-01 nipkow 2011-12-01 merged IMP/Util into IMP/Vars
2011-11-29 wenzelm 2011-11-29 more conventional file name;
2011-11-18 bulwahn 2011-11-18 adding another example for lifting definitions
2011-11-17 bulwahn 2011-11-17 adding a preliminary example to show how the quotient_definition package can be generalized
2011-11-14 hoelzl 2011-11-14 add Code_Real_Approx_By_Float
2011-11-06 wenzelm 2011-11-06 more precise dependencies;
2011-11-03 kleing 2011-11-03 moved latex generation for HOL-IMP out of distribution
2011-11-01 bulwahn 2011-11-01 renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
2011-10-25 bulwahn 2011-10-25 renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
2011-10-24 nipkow 2011-10-24 latex output not needed because errors manifest themselves earlier
2011-10-22 nipkow 2011-10-22 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
2011-10-21 huffman 2011-10-21 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
2011-10-19 bulwahn 2011-10-19 removing old code generator
2011-10-19 bulwahn 2011-10-19 removing old code generator for inductive predicates
2011-10-19 bulwahn 2011-10-19 removing old code generator setup in the HOL theory
2011-10-19 bulwahn 2011-10-19 removing invocations of the evaluation method based on the old code generator
2011-09-28 nipkow 2011-09-28 Added dependecies
2011-09-28 nipkow 2011-09-28 Added Hoare-like Abstract Interpretation
2011-09-28 nipkow 2011-09-28 moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
2011-09-26 wenzelm 2011-09-26 reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
2011-09-25 haftmann 2011-09-25 Quotient_Set.thy is part of library
2011-09-24 sultana 2011-09-24 fixed IsaMakefile action for HOL-TPTP.
2011-09-22 berghofe 2011-09-22 Moved extraction part of Higman's lemma to separate theory to allow reuse in theories compiled without support for proof terms.
2011-09-22 berghofe 2011-09-22 Added documentation for HOL-SPARK
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2011-09-21 nipkow 2011-09-21 added missing makefile dependence
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.
2011-09-18 wenzelm 2011-09-18 finite sequences as useful as introductory example;
2011-09-13 bulwahn 2011-09-13 correcting theory name and dependencies
2011-09-12 bulwahn 2011-09-12 moving connection of association lists to Mappings into a separate theory
2011-09-10 haftmann 2011-09-10 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie
2011-09-02 nipkow 2011-09-02 merged
2011-09-02 nipkow 2011-09-02 Added Abstract Interpretation theories
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-08-24 huffman 2011-08-24 move everything related to 'norm' method into new theory file Norm_Arith.thy
2011-08-21 krauss 2011-08-21 removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
2011-08-18 huffman 2011-08-18 add Multivariate_Analysis dependencies
2011-08-18 haftmann 2011-08-18 avoid case-sensitive name for example theory
2011-08-17 huffman 2011-08-17 IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
2011-08-17 wenzelm 2011-08-17 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-11 krauss 2011-08-11 removed obsolete recdef-related examples
2011-08-10 wenzelm 2011-08-10 moved old code generator to src/Tools/;
2011-08-09 blanchet 2011-08-09 load lambda-lifting structure earlier, so it can be used in Metis
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-08-01 huffman 2011-08-01 new theory HOL/Library/Product_Lattice.thy
2011-07-26 bulwahn 2011-07-26 more precise dependencies
2011-07-25 bulwahn 2011-07-25 removing SML_Quickcheck
2011-07-20 boehmes 2011-07-20 more precise dependencies
2011-07-20 boehmes 2011-07-20 merged
2011-07-20 boehmes 2011-07-20 removed old (unused) SMT monomorphizer
2011-07-20 hoelzl 2011-07-20 merged
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-07-19 hoelzl 2011-07-19 rename Nat_Infinity (inat) to Extended_Nat (enat)
2011-07-20 Cezary Kaliszyk 2011-07-20 HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.