src/ZF/Nat.ML
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Wed, 27 Jan 1999 10:31:31 +0100 paulson new typechecking solver for the simplifier
Thu, 07 Jan 1999 18:30:55 +0100 paulson ZF: the natural numbers as a datatype
Tue, 22 Sep 1998 13:50:57 +0200 paulson tidying
Fri, 18 Sep 1998 15:09:46 +0200 paulson tidied
Fri, 11 Sep 1998 16:25:40 +0200 paulson fixed PROOF FAILED
Mon, 17 Aug 1998 13:09:08 +0200 paulson Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
Wed, 15 Jul 1998 14:13:18 +0200 paulson More tidying and removal of "\!\!... from Goal commands
Mon, 13 Jul 1998 16:43:57 +0200 paulson Huge tidy-up: removal of leading \!\!
Mon, 22 Jun 1998 17:12:27 +0200 wenzelm isatool fixgoal;
Thu, 20 Nov 1997 11:03:53 +0100 paulson Speeded up the proof of succ_lt_induct_lemma
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Thu, 10 Apr 1997 10:55:37 +0200 paulson Changed some fast_tac to blast_tac
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Thu, 26 Sep 1996 15:14:23 +0200 paulson Ran expandshort; used stac instead of ssubst
Thu, 05 Sep 1996 18:30:13 +0200 paulson Renaming of _rews to _simps
Tue, 26 Mar 1996 11:45:54 +0100 paulson Updated comments
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 23 Dec 1994 16:30:35 +0100 lcp natE0: deleted, since unused
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
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
Mon, 15 Nov 1993 14:41:25 +0100 lcp changed all co- and co_ to co
Wed, 06 Oct 1993 09:58:53 +0100 lcp Retrying yet again after network problems
Thu, 30 Sep 1993 10:26:38 +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
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip