src/HOL/ex/ROOT.ML
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
1997-04-18 paulson 1997-04-18 Now loads theory LList indirectly: via LFilter
1996-11-29 nipkow 1996-11-29 Moved the Rings stuff from ex to Integ and showed that int::cring.
1996-11-26 nipkow 1996-11-26 Added Lagrang. Modified comment.
1996-06-14 paulson 1996-06-14 Added new Primes theory
1996-05-06 paulson 1996-05-06 Now mentions but does not load mesontest2.ML
1996-04-04 paulson 1996-04-04 New example Comb: Church-Rosser for combinators, ported from ZF
1996-03-27 paulson 1996-03-27 New mutilated checkerboard example
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-11-21 clasohm 1995-11-21 removed make_chart; theories are now read from the current directory (because of use_dir)
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-06-30 lcp 1995-06-30 added mention of new theories BT and Perm
1995-06-29 clasohm 1995-06-29 renamed CHOL to HOL
1995-04-10 nipkow 1995-04-10 ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. MT.thy: Deleted extra space in clos_mk.
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-22 clasohm 1995-03-22 fixed bug: HOL_build_completed replaced by CHOL_build_completed
1995-03-22 clasohm 1995-03-22 converted ex with curried function application