2012-03-26 wenzelm 2012-03-26 disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-17 wenzelm 2012-03-17 renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
2012-03-15 wenzelm 2012-03-15 more precise TPTP keywords and dependencies;
2012-03-07 wenzelm 2012-03-07 some recovery of IsaMakefile targets from f3c10e908f65;
2012-03-04 haftmann 2012-03-04 move test targets to test target
2012-03-04 haftmann 2012-03-04 dropped images for importer sessions
2012-03-04 haftmann 2012-03-04 more accurate dependencies
2012-03-03 haftmann 2012-03-03 added actual dependencies
2012-03-03 haftmann 2012-03-03 switch of target Import-HOL_Light-Imported: not operative at the moment
2012-03-03 haftmann 2012-03-03 formal infrastructure for import sessions
2012-02-27 wenzelm 2012-02-27 removed dead code (cf. a34d89ce6097);
2012-02-27 wenzelm 2012-02-27 reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository; moved the whole HOL-Quickcheck_Examples target from "all" to "full" for now -- it does not terminate in certain situations (to be investigated further);
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 wenzelm 2012-02-24 more precise clean target;
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-22 bulwahn 2012-02-22 NEWS
2012-02-22 bulwahn 2012-02-22 adding some examples with find_unused_assms command
2012-02-22 bulwahn 2012-02-22 moving Quickcheck's example to its own session
2012-02-21 huffman 2012-02-21 renamed ex/Numeral.thy to ex/Numeral_Representation.thy
2012-02-02 bulwahn 2012-02-02 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2012-01-23 blanchet 2012-01-23 added problem importer
2012-01-23 blanchet 2012-01-23 renamed theory exporter
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