src/ZF/Arith.ML
Fri, 17 May 2002 16:47:24 +0200 paulson deleting the obsolete theorem lt_succ_iff
Thu, 17 Jan 2002 12:45:52 +0100 paulson new definitions from Sidi Ehmety
Tue, 26 Jun 2001 17:25:41 +0200 paulson a few new and/or improved results
Thu, 07 Sep 2000 21:12:49 +0200 wenzelm tuned ML code (the_context, bind_thms(s));
Mon, 07 Aug 2000 10:29:54 +0200 paulson instantiated Cancel_Numerals for "nat" in ZF
Tue, 01 Aug 2000 18:26:34 +0200 paulson used natify with div and mod; also put in the divide-by-zero trick
Tue, 01 Aug 2000 15:28:21 +0200 paulson natify, a coercion to reduce the number of type constraints in arithmetic
Thu, 13 Jul 2000 12:59:26 +0200 paulson removed needless premises
Wed, 22 Mar 2000 12:45:41 +0100 paulson tidied using new "inst" rule
Mon, 07 Feb 2000 15:14:02 +0100 paulson tidied some proofs
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Tue, 07 Sep 1999 10:40:58 +0200 wenzelm isatool expandshort;
Fri, 29 Jan 1999 17:08:20 +0100 paulson expandshort
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
Thu, 07 Jan 1999 10:56:05 +0100 paulson if-then-else syntax for ZF
Tue, 22 Sep 1998 13:50:57 +0200 paulson tidying
Fri, 18 Sep 1998 15:09:26 +0200 paulson new theorem less_imp_Suc_add
Wed, 19 Aug 1998 10:37:07 +0200 paulson new theorem zero_less_diff
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 \!\!
Thu, 02 Jul 1998 17:58:12 +0200 paulson Renamed expand_if to split_if and setloop split_tac to addsplits,
Mon, 22 Jun 1998 17:12:27 +0200 wenzelm isatool fixgoal;
Tue, 28 Apr 1998 13:50:41 +0200 paulson new thm mult_lt_mono1
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Fri, 10 Oct 1997 18:23:31 +0200 wenzelm fixed dots;
Mon, 29 Sep 1997 11:56:04 +0200 paulson Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
Thu, 15 May 1997 15:51:47 +0200 oheimb renamed unsafe_addss to addss
Wed, 23 Apr 1997 10:54:22 +0200 paulson Conversion to use blast_tac
Sat, 15 Feb 1997 17:52:31 +0100 oheimb reflecting my recent changes of the simplifier and classical reasoner
Wed, 08 Jan 1997 15:04:27 +0100 paulson Removal of sum_cs and eq_cs
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, 13 Jun 1996 16:22:37 +0200 paulson New example of GCDs and divides relation
Wed, 01 May 1996 10:35:06 +0200 paulson tidied some proofs
Thu, 28 Mar 1996 10:52:59 +0100 paulson Ran expandshort
Tue, 26 Mar 1996 11:42:36 +0100 paulson New lemmas for Mutilated Checkerboard
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
Thu, 23 Jun 1994 17:38:12 +0200 lcp modifications for cardinal arithmetic
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Thu, 18 Nov 1993 14:57:05 +0100 lcp Misc modifs such as expandshort
Tue, 05 Oct 1993 15:21:29 +0100 lcp ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
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
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip