src/HOL/ex/ROOT.ML
2009-03-23 ago moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-11 ago moved Decision_Procs examples to Decision_Procs/ex
2009-03-08 ago added predicate compiler, as formally checked prototype, not as user package
2009-02-28 ago A Serbian theory, by Filip Maric.
2009-02-05 ago split of already properly working part of Quickcheck infrastructure
2009-02-03 ago established session HOL-Reflection
2009-02-03 ago repaired accidental commit
2009-02-01 ago merged
2009-02-01 ago added State_Monad theory in session
2009-01-30 ago Added Formal_Power_Series_Examples to HOL-ex image
2009-01-28 ago Reflection.thy now in HOL/Library
2009-01-06 ago more parallel loading;
2009-01-06 ago more parallel loading;
2008-12-27 ago renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-11-20 ago reactivated some dead theories (based on hints by Mark Hillebrand);
2008-10-16 ago removed Locales;
2008-09-25 ago (temporary workaround)
2008-09-25 ago (temporal deactivation)
2008-09-22 ago Added examples for coherent logic prover.
2008-09-17 ago moved global ML bindings to global place;
2008-09-16 ago moved term_of syntax to separate theory
2008-09-16 ago evaluation using code generator
2008-09-03 ago removed ex/Puzzle
2008-09-03 ago retired Ben Porter's DenumRat in favour of the shorter proof in
2008-09-02 ago Replaced Library/NatPair by Nat_Int_Bij.
2008-08-27 ago added HOL/ex/Numeral.thy
2008-08-05 ago fix HOL/ex/LexOrds.thy; add to regression
2008-07-25 ago tuned
2008-07-03 ago removed old NSPrimes, cf. NSA/Examples/;
2008-07-02 ago code antiquotation roaring ahead
2008-07-01 ago HOL += HOL-Complex
2008-03-12 ago separated Random.thy from Quickcheck.thy
2008-02-20 ago removed NBE;
2008-01-25 ago Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
2008-01-25 ago distinguished examples for Efficient_Nat.thy
2007-12-20 ago included meson/metis tests in simultaneous use_thys;
2007-12-07 ago Adding "ex/Induction_Scheme.thy" to tests
2007-12-05 ago dropped Classpackage.thy
2007-11-10 ago qualified Proofterm.proofs;
2007-10-12 ago consolidated naming conventions for code generator theories
2007-10-11 ago enabled Refute_Examples again;
2007-10-11 ago disabled Refute_Examples temporarily;
2007-09-27 ago some more simultaneous use_thys;
2007-09-18 ago Added function package to PreList
2007-09-06 ago Integrated Executable_Rat and Executable_Real theories into
2007-09-05 ago tuned;
2007-08-29 ago some simultaneous use_thys;
2007-08-09 ago tuned
2007-08-02 ago converted Meson tests to proper theory;
2007-07-19 ago uniform naming conventions for CG theories
2007-07-16 ago fixed SML/NJ int problem
2007-06-26 ago added NBE
2007-06-21 ago replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
2007-06-10 ago disabled theory "Reflected_Presburger" for smlnj (temporarily);
2007-06-05 ago tuned document;
2007-06-01 ago some tests for arith added
2007-06-01 ago MiniSAT mentioned in comment
2007-05-17 ago Added unification case study (using new function package)
2007-04-13 ago New file for locale regression tests.