src/HOL/ex/ROOT.ML
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
2007-01-22 krauss 2007-01-22 Included ex/Fundefs.thy in HOL-ex session
2007-01-20 wenzelm 2007-01-20 added HOL/ex/Binary.thy;
2007-01-16 haftmann 2007-01-16 refined and added example for ExecutableRat
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-10-06 kleing 2006-10-06 examples for hex and bin numerals
2006-10-01 wenzelm 2006-10-01 reactivated theory PER; removed obsolete StringEx;
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-08-30 haftmann 2006-08-30 added yet another code generator example
2006-08-29 haftmann 2006-08-29 added and refined some exmples
2006-08-21 haftmann 2006-08-21 added some codegen examples/applications
2006-08-03 wenzelm 2006-08-03 added HOL/ex/Reflection;
2006-07-04 wenzelm 2006-07-04 added ex/Guess.thy;
2006-06-09 nipkow 2006-06-09 nbe -> NormalForm
2006-04-13 wenzelm 2006-04-13 early test of Classpackage, Codegenerator;
2006-03-17 haftmann 2006-03-17 added example for operational classes and code generator
2006-03-11 wenzelm 2006-03-11 nbe: no_document;
2006-02-27 nipkow 2006-02-27 added temp. nbe test
2006-02-16 wenzelm 2006-02-16 added ex/Abstract_NAT.thy;
2006-02-12 kleing 2006-02-12 * moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-14 webertj 2005-12-14 ex/Sudoku.thy
2005-10-07 wenzelm 2005-10-07 removed obsolete ex/Tuple.thy;
2005-09-23 webertj 2005-09-23 new sat tactic imports resolution proofs from zChaff
2005-09-20 wenzelm 2005-09-20 Chinese Unicode example;
2005-09-17 wenzelm 2005-09-17 Hebrew: HTML.with_charset;
2005-09-15 wenzelm 2005-09-15 added Hebrew.thy;
2005-09-14 chaieb 2005-09-14 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring
2005-04-28 bauerg 2005-04-28 *** empty log message ***