src/HOL/ex/ROOT.ML
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 ***
2004-07-12 nipkow 2004-07-12 *** empty log message ***
2004-04-16 nipkow 2004-04-16 Moved ring stuff from ex into Ring_and_Field.
2004-04-16 berghofe 2004-04-16 Added theory with examples for quickcheck command.
2004-04-15 nipkow 2004-04-15 Added ex/Exceptions.thy
2004-03-29 skalberg 2004-03-29 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.
2004-03-25 kleing 2004-03-25 moved MiniML and AVL to archive of formal proofs
2004-03-11 webertj 2004-03-11 Refute_Examples added/fixed
2004-03-10 webertj 2004-03-10 added Refute_Examples.thy
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions
2003-10-08 paulson 2003-10-08 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
2003-03-25 berghofe 2003-03-25 Added examples for Presburger arithmetic.
2002-06-03 nipkow 2002-06-03 Added ex/MergeSort
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;
2001-12-10 berghofe 2001-12-10 Added example file for intuitionistic logic (taken from FOL).
2001-12-04 wenzelm 2001-12-04 added Higher_Order_Logic.thy;
2001-11-23 wenzelm 2001-11-23 time_use_thy "Locales";
2001-11-22 wenzelm 2001-11-22 theory Locales temporarily disabled;
2001-11-09 wenzelm 2001-11-09 back to normal; tuned;
2001-11-08 wenzelm 2001-11-08 tuned;
2001-11-06 wenzelm 2001-11-06 use_thy "Locales";
2001-09-27 wenzelm 2001-09-27 tuned;
2001-07-23 paulson 2001-07-23 PiSets moved to GroupTheory, while LocaleGroup deleted
2000-11-10 wenzelm 2000-11-10 proper theory context for mesontest2;
2000-09-21 wenzelm 2000-09-21 renamed HOL/ex/Points to HOL/ex/Records;
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization to HOL/NumberTheory