src/ZF/ROOT.ML
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Thu, 11 Mar 1999 13:20:35 +0100 wenzelm removed foo_build_completed -- now handled by session management (via usedir);
Mon, 08 Feb 1999 17:30:22 +0100 wenzelm ~~;
Wed, 27 Jan 1999 10:31:31 +0100 paulson new typechecking solver for the simplifier
Wed, 13 Jan 1999 11:57:09 +0100 paulson datatype package improvements
Fri, 08 Jan 1999 13:20:59 +0100 paulson removal of DO_GOAL
Thu, 07 Jan 1999 18:30:55 +0100 paulson ZF: the natural numbers as a datatype
Wed, 06 Jan 1999 13:24:33 +0100 paulson induct_tac and exhaust_tac
Mon, 28 Dec 1998 16:59:28 +0100 paulson new inductive, datatype and primrec packages, etc.
Tue, 22 Sep 1998 13:50:57 +0200 paulson tidying
Fri, 18 Sep 1998 16:07:55 +0200 paulson leaves subgoal package empty
Fri, 21 Nov 1997 15:29:56 +0100 wenzelm changed Pure/Sequence interface -- isatool fixseq;
Thu, 20 Nov 1997 16:24:05 +0100 wenzelm $ISABELLE_HOME/src;
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Fri, 16 Feb 1996 18:00:47 +0100 paulson Elimination of fully-functorial style.
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Tue, 21 Nov 1995 15:10:12 +0100 clasohm main directory is now read by exit_use_dir, too;
Tue, 24 Oct 1995 14:50:24 +0100 clasohm added calls of init_html and make_chart
Tue, 25 Apr 1995 10:56:49 +0200 lcp Now loads the theory "Let". Could add it to FOL, but this appears to
Fri, 16 Dec 1994 18:07:12 +0100 lcp changed useless "qed" calls for lemmas back to uses of "result",
Thu, 25 Aug 1994 12:09:21 +0200 lcp ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
Tue, 16 Aug 1994 18:58:42 +0200 lcp ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Wed, 27 Jul 1994 15:33:42 +0200 lcp Addition of infinite branching datatypes
Tue, 26 Jul 1994 13:21:20 +0200 lcp Axiom of choice, cardinality results, etc.
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Fri, 06 May 1994 15:16:11 +0200 lcp renaming/removal of filenames to correct case
Tue, 16 Nov 1993 14:24:21 +0100 clasohm made pseudo theories for all ML files;
Mon, 15 Nov 1993 14:41:25 +0100 lcp changed all co- and co_ to co
Thu, 04 Nov 1993 14:11:59 +0100 clasohm renamed some files
Fri, 22 Oct 1993 13:43:45 +0100 clasohm added -h 15000 for Poly/ML in Makefile,
Mon, 11 Oct 1993 13:58:22 +0100 clasohm renamed ordinal.* to ord.*
Wed, 06 Oct 1993 14:19:39 +0100 clasohm changed "list-fn" to "listfn"
Thu, 30 Sep 1993 10:10:21 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Fri, 17 Sep 1993 16:16:38 +0200 lcp Installation of new simplifier for ZF. Deleted all congruence rules not
Fri, 17 Sep 1993 12:53:53 +0200 lcp test commit
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip