src/HOL/ex/ROOT.ML
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