src/ZF/ex/ROOT.ML
Wed, 14 Nov 2001 23:21:05 +0100 wenzelm removed BT, Data, Enum (see ZF/Induct);
Wed, 07 Nov 2001 12:29:07 +0100 paulson reorganization of the ZF examples
Fri, 06 Jul 2001 16:04:32 +0200 paulson two Isar tactic scripts
Sat, 03 Feb 2001 12:41:38 +0100 paulson commutation theory, ported by Sidi Ehmety
Fri, 18 Aug 2000 12:31:20 +0200 paulson new example ZF/ex/NatSum
Tue, 30 May 2000 16:08:38 +0200 wenzelm cleaned up;
Thu, 11 Mar 1999 13:20:35 +0100 wenzelm removed foo_build_completed -- now handled by session management (via usedir);
Mon, 28 Dec 1998 16:53:24 +0100 paulson fixed comment
Tue, 22 Sep 1998 15:24:39 +0200 paulson re-organized for the new directory Integ
Fri, 19 Dec 1997 10:18:03 +0100 wenzelm tuned;
Wed, 27 Nov 1996 13:01:07 +0100 paulson Better indentation
Thu, 13 Jun 1996 16:22:37 +0200 paulson New example of GCDs and divides relation
Tue, 26 Mar 1996 12:01:13 +0100 paulson Now loads Mutil example
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Tue, 21 Nov 1995 12:43:09 +0100 clasohm removed make_chart;
Tue, 24 Oct 1995 14:50:24 +0100 clasohm added calls of init_html and make_chart
Mon, 16 Oct 1995 16:32:56 +0100 paulson Added the new Limit.{thy,ML} example
Thu, 16 Mar 1995 00:00:30 +0100 lcp Removed exception handlers, as they are now in ZF/Makefile.
Tue, 28 Feb 1995 10:53:56 +0100 lcp No longer calls maketest; instead, the Makefile writes the file
Wed, 07 Sep 1994 17:28:53 +0200 lcp addition of ZF/ex/twos_compl.thy
Wed, 17 Aug 1994 10:38:37 +0200 lcp ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
Mon, 15 Aug 1994 18:27:50 +0200 lcp ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
Fri, 12 Aug 1994 12:28:46 +0200 lcp installation of new inductive/datatype sections
Wed, 27 Jul 1994 16:03:16 +0200 lcp Addition of infinite branching datatypes
Fri, 06 May 1994 15:35:35 +0200 lcp renaming/removal of filenames to correct case
Wed, 01 Dec 1993 17:40:27 +0100 lcp ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
Tue, 16 Nov 1993 14:26:15 +0100 clasohm changed use_thy's parameter to exact theory name
Mon, 15 Nov 1993 14:41:25 +0100 lcp changed all co- and co_ to co
Mon, 08 Nov 1993 17:52:24 +0100 lcp Minor changes; addition of counit.ML
Thu, 04 Nov 1993 14:12:31 +0100 clasohm renamed twos-compl.ML to twos_compl.ML
Fri, 22 Oct 1993 13:44:27 +0100 clasohm renamed some files
Fri, 15 Oct 1993 10:25:23 +0100 lcp ZF/ex/tf/tree,forest_unfold: streamlined the proofs
Wed, 06 Oct 1993 14:45:04 +0100 clasohm changed filenames to lower case name of theory the file contains
Thu, 30 Sep 1993 10:54:01 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip