src/ZF/ex/ROOT.ML
2000-05-30 wenzelm 2000-05-30 cleaned up;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1998-12-28 paulson 1998-12-28 fixed comment
1998-09-22 paulson 1998-09-22 re-organized for the new directory Integ
1997-12-19 wenzelm 1997-12-19 tuned;
1996-11-27 paulson 1996-11-27 Better indentation
1996-06-13 paulson 1996-06-13 New example of GCDs and divides relation
1996-03-26 paulson 1996-03-26 Now loads Mutil 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-10-16 paulson 1995-10-16 Added the new Limit.{thy,ML} example
1995-03-16 lcp 1995-03-16 Removed exception handlers, as they are now in ZF/Makefile.
1995-02-28 lcp 1995-02-28 No longer calls maketest; instead, the Makefile writes the file test.
1994-09-07 lcp 1994-09-07 addition of ZF/ex/twos_compl.thy
1994-08-17 lcp 1994-08-17 ZF/ex/ROOT: added .ML to use command use "ex/twos_compl" Should be able to delete this after fixing the treatment of orphans.
1994-08-15 lcp 1994-08-15 ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; removed some explicit loads by exploiting theory dependencies
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-27 lcp 1994-07-27 Addition of infinite branching datatypes
1994-05-06 lcp 1994-05-06 renaming/removal of filenames to correct case
1993-12-01 lcp 1993-12-01 ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted them, to make the most of the load-path mechanism. (use_thy adds the new theory to the list of loaded theories.)
1993-11-16 clasohm 1993-11-16 changed use_thy's parameter to exact theory name
1993-11-15 lcp 1993-11-15 changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs
1993-11-08 lcp 1993-11-08 Minor changes; addition of counit.ML
1993-11-04 clasohm 1993-11-04 renamed twos-compl.ML to twos_compl.ML
1993-10-22 clasohm 1993-10-22 renamed some files
1993-10-15 lcp 1993-10-15 ZF/ex/tf/tree,forest_unfold: streamlined the proofs Updated other inductive def examples as per changes in the package.
1993-10-06 clasohm 1993-10-06 changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split)
1993-09-30 lcp 1993-09-30 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed called expandshort
1993-09-16 clasohm 1993-09-16 Initial revision