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