src/HOL/IsaMakefile
2012-05-18 blanchet 2012-05-18 added a timeout to "try0" in Mirabelle
2012-04-27 blanchet 2012-04-27 get rid of old CASC setup and move the arithmetic part to a new theory
2012-04-27 blanchet 2012-04-27 move file to where it belongs
2012-04-24 sultana 2012-04-24 reversed Tools to Actions Mirabelle renaming;
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer
2012-04-21 huffman 2012-04-21 new example theory for transfer package
2012-04-19 nipkow 2012-04-19 added revised version of Abs_Int
2012-04-19 nipkow 2012-04-19 reorganised IMP
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-14 sultana 2012-04-14 renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
2012-04-14 krauss 2012-04-14 removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-04-03 huffman 2012-04-03 renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03 huffman 2012-04-03 merged
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-04-03 wenzelm 2012-04-03 some context examples;
2012-04-01 krauss 2012-04-01 merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
2012-04-01 krauss 2012-04-01 renamed import session back to Import, conforming to directory name; NEWS
2012-04-01 wenzelm 2012-04-01 more precise IsaMakefile (eg. see HOL-Algebra);
2012-04-01 krauss 2012-04-01 merged
2012-04-01 krauss 2012-04-01 removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare
2012-04-01 Cezary Kaliszyk 2012-04-01 Modernized HOL-Import for HOL Light
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-30 haftmann 2012-03-30 dropped now obsolete Cset theories
2012-03-30 huffman 2012-03-30 remove content-free theory ex/Arithmetic_Series_Complex.thy
2012-03-30 bulwahn 2012-03-30 adding theory to prove completeness of the exhaustive generators
2012-03-26 huffman 2012-03-26 revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
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