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