2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-12 hoelzl 2015-04-12 move filters to their own theory
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-23 haftmann 2014-10-23 further downshift of theory Parity in the hierarchy
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-16 blanchet 2014-09-16 tuned fact visibility
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-03 blanchet 2014-09-03 tuned imports
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-08-28 blanchet 2014-08-28 moved old 'smt' method out of 'Main'
2014-07-24 wenzelm 2014-07-24 more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-06-11 blanchet 2014-06-11 removed old SMT module from Sledgehammer
2014-03-21 traytel 2014-03-21 simplified internal datatype construction
2014-03-11 blanchet 2014-03-11 moved 'Quickcheck_Narrowing' further down the theory graph
2014-02-19 traytel 2014-02-19 reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
2014-02-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-01-23 blanchet 2014-01-23 hide 'csum' etc.
2014-01-20 blanchet 2014-01-20 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
2014-01-20 blanchet 2014-01-20 hide BNF notation
2014-01-20 blanchet 2014-01-20 removed dependency of BNF package on Nitpick
2014-01-20 blanchet 2014-01-20 deactivate one more cardinal notation
2014-01-20 blanchet 2014-01-20 moved hide_const from BNF to Main
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 compile
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'
2014-01-20 blanchet 2014-01-20 kill notations
2014-01-20 blanchet 2014-01-20 renamed '_FP' files to 'BNF_' files
2014-01-20 blanchet 2014-01-20 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
2014-01-16 blanchet 2014-01-16 moved 'Zorn' into 'Main', since it's a BNF dependency
2013-11-21 blanchet 2013-11-21 moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
2013-11-20 blanchet 2013-11-20 moved 'coinduction' proof method to 'HOL'
2013-11-20 blanchet 2013-11-20 factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-01-07 haftmann 2012-01-07 dropped theory More_Set
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-09-10 haftmann 2011-09-10 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-08-20 haftmann 2011-08-20 compatibility layer
2011-05-05 bulwahn 2011-05-05 adding creation of exhaustive generators for records; simplifying dependencies in Main theory
2011-03-11 bulwahn 2011-03-11 correcting dependencies after renaming
2010-11-08 bulwahn 2010-11-08 adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-10-26 blanchet 2010-10-26 integrated "smt" proof method with Sledgehammer
2010-10-26 blanchet 2010-10-26 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-08-12 haftmann 2010-08-12 group record-related ML files
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.
2010-01-14 blanchet 2010-01-14 reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2009-10-29 blanchet 2009-10-29 readded Predicate_Compile to Main
2009-10-28 blanchet 2009-10-28 merged my Auto Nitpick change with Lukas's Predicate Compiler changes
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian