2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2012-01-23 blanchet 2012-01-23 rebranded Nitrox, for more uniformity
2012-01-17 bulwahn 2012-01-17 renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
2012-01-17 bulwahn 2012-01-17 renamed theory AList to DAList
2012-01-16 nipkow 2012-01-16 missing dependency
2012-01-10 bulwahn 2012-01-10 adding theory association lists with invariant
2012-01-07 haftmann 2012-01-07 dropped theory More_Set
2012-01-06 haftmann 2012-01-06 farewell to theory More_List
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-12-26 haftmann 2011-12-26 dropped Executable_Set wrapper theory
2011-12-17 wenzelm 2011-12-17 clarified modules that contribute to datatype package;
2011-12-16 wenzelm 2011-12-16 clarified modules that contribute to datatype package;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-12-15 nipkow 2011-12-15 merged
2011-12-15 nipkow 2011-12-15 tuned
2011-12-14 blanchet 2011-12-14 added new proof redirection code
2011-12-14 bulwahn 2011-12-14 correcting dependencies after renaming
2011-12-14 wenzelm 2011-12-14 more visible benchmarks; uniform IsaMakefile target "full" to cover such extra sessions;
2011-12-11 nipkow 2011-12-11 added IMP/Live_True.thy
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