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