src/HOL/ex/ROOT.ML
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
2000-09-05 paulson 2000-09-05 meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
2000-07-16 wenzelm 2000-07-16 added Tuple.thy;
2000-07-13 wenzelm 2000-07-13 tuned;
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-05-30 wenzelm 2000-05-30 cleaned up;
2000-05-24 paulson 2000-05-24 restored NatSum.thy
2000-05-23 paulson 2000-05-23 theory file NatSum.thy no longer needed
2000-05-05 nipkow 2000-05-05 Added AVL
2000-03-24 wenzelm 2000-03-24 added HOL/ex/Multiquote.thy;
2000-03-23 paulson 2000-03-23 restored the MESON examples file HOL/ex/mesontest2.ML
2000-03-08 paulson 2000-03-08 new theory ex/Factorization
1999-08-20 wenzelm 1999-08-20 if_svc_enabled;
1999-08-06 paulson 1999-08-06 svc_enabled is now declared as a function
1999-08-06 paulson 1999-08-06 new theory ex/svc_test.thy
1999-08-03 paulson 1999-08-03 new examples file for SVC
1999-07-26 paulson 1999-07-26 HOL/ex/Tarski: new example by Florian Kammueller
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1998-11-16 paulson 1998-11-16 removed the reference to mesontest2.ML, itself now deleted
1998-10-23 wenzelm 1998-10-23 tuned;
1998-08-24 wenzelm 1998-08-24 added Antiquote example;
1998-08-04 wenzelm 1998-08-04 added LocaleGroup, PiSets examples;
1998-07-24 wenzelm 1998-07-24 added ex/MonoidGroups (record example); moved Bin and String examples to ex;
1998-07-03 wenzelm 1998-07-03 stepping stones: Recdef, Main; String now part of main HOL;
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real
1998-04-20 paulson 1998-04-20 proving fib(gcd(m,n)) = gcd(fib m, fib n)
1997-12-19 wenzelm 1997-12-19 tuned;
1997-06-05 paulson 1997-06-05 Now loads theory Recdef
1997-05-26 paulson 1997-05-26 Primrec: New example ported from ZF
1997-05-22 paulson 1997-05-22 New example: ex/Fib
1997-05-20 paulson 1997-05-20 Removal of ex/LexProd
1997-05-07 paulson 1997-05-07 Moved induction examples to directory Induct