src/HOL/Nat.ML
Tue, 06 Sep 2005 16:59:48 +0200 wenzelm axclass: name space prefix is now "c_class" instead of just "c";
Wed, 13 Jul 2005 15:06:20 +0200 paulson generlization of some "nat" theorems
Wed, 04 May 2005 08:36:10 +0200 nipkow Fixing a problem with lin.arith.
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
Mon, 29 Nov 2004 14:02:55 +0100 paulson converted to Isar script, simplifying some results
Sat, 27 Dec 2003 21:02:14 +0100 paulson re-organized numeric lemmas
Mon, 05 Aug 2002 14:27:55 +0200 berghofe Legacy ML bindings.
Wed, 31 Jul 2002 16:10:24 +0200 nipkow added mk_left_commute to HOL.thy and used it "everywhere"
Thu, 25 Apr 2002 17:36:29 +0200 nipkow added "m <= n ==> m-n = 0" [simp]
Tue, 26 Feb 2002 13:37:48 +0100 paulson Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
Mon, 25 Feb 2002 10:42:34 +0100 nipkow solved the problem that Larry's simproce cancle_numerals(?) returns
Thu, 13 Dec 2001 15:45:03 +0100 wenzelm isatool expandshort;
Mon, 22 Oct 2001 11:54:22 +0200 paulson Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Mon, 06 Aug 2001 13:43:24 +0200 nipkow turned translation for 1::nat into def.
Thu, 31 May 2001 16:50:13 +0200 oheimb added Least_Suc2
Thu, 15 Feb 2001 16:01:07 +0100 oheimb moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
Wed, 10 Jan 2001 11:14:30 +0100 paulson generalizing the LEAST theorems from "nat" to linear
Wed, 20 Dec 2000 12:14:26 +0100 paulson tidying, removing obsolete lemmas about 0=... and 1=...
Fri, 01 Dec 2000 11:02:55 +0100 paulson renamed less_eq_Suc_add to less_imp_Suc_add
Fri, 10 Nov 2000 19:18:14 +0100 wenzelm nat_distrib;
Mon, 09 Oct 2000 12:24:12 +0200 paulson got rid of a swap
Fri, 15 Sep 2000 12:39:57 +0200 paulson renamed (most of...) the select rules
Wed, 06 Sep 2000 08:04:41 +0200 nipkow less_induct -> nat_less_induct
Thu, 17 Aug 2000 12:02:01 +0200 paulson better rules for cancellation of common factors across comparisons
Tue, 25 Jul 2000 00:06:46 +0200 wenzelm rearranged setup of arithmetic procedures, avoiding global reference values;
Thu, 22 Jun 2000 23:04:34 +0200 wenzelm bind_thm(s);
Tue, 23 May 2000 18:28:11 +0200 paulson added type constraint ::nat because 0 is now overloaded
Mon, 13 Mar 2000 16:23:34 +0100 wenzelm case_tac now subsumes both boolean and datatype cases;
Mon, 13 Mar 2000 12:51:10 +0100 nipkow exhaust_tac -> cases_tac
Fri, 18 Feb 2000 20:24:56 +0100 oheimb added Suc_le_D
Mon, 10 Jan 2000 16:06:43 +0100 nipkow Forgot to "call" MicroJava in makefile.
Tue, 27 Jul 1999 17:19:31 +0200 paulson expandshort and tidying
Wed, 21 Jul 1999 15:23:18 +0200 paulson removed 2 qed_goals
Thu, 10 Jun 1999 10:34:55 +0200 paulson new lemma less_Suc_eq_0_disj
Thu, 15 Apr 1999 18:10:37 +0200 nipkow Added new thms.
Wed, 03 Mar 1999 11:15:18 +0100 paulson expandshort
Wed, 13 Jan 1999 12:16:34 +0100 nipkow Refined arithmetic.
Wed, 13 Jan 1999 08:41:28 +0100 nipkow Simplified arithmetic.
Fri, 27 Nov 1998 17:00:30 +0100 nipkow At last: linear arithmetic for nat!
Wed, 14 Oct 1998 11:50:48 +0200 nipkow Nat: added zero_neq_conv
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Fri, 24 Jul 1998 13:34:59 +0200 berghofe Declaration of type 'nat' as a datatype (this allows usage of
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Wed, 23 Apr 1997 11:18:29 +0200 paulson Ran expandshort
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes.
Wed, 18 Dec 1996 15:10:33 +0100 oheimb added nat_induct2
Thu, 28 Nov 1996 12:09:33 +0100 nipkow Missing case in instantiation of Transitivity prover (negate(None)=None)
Thu, 07 Nov 1996 10:11:06 +0100 paulson Adding lessI to default claset
Mon, 21 Oct 1996 09:50:50 +0200 nipkow Added trans_tac (see Provers/nat_transitive.ML)
Wed, 16 Oct 1996 10:37:17 +0200 nipkow Defined pred using nat_case rather than nat_rec.
Thu, 10 Oct 1996 10:45:20 +0200 paulson Removed Fast_tac made redundant by addition of de Morgan laws
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Mon, 23 Sep 1996 18:12:45 +0200 paulson Addition of le_refl to default simpset/claset
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
Wed, 21 Aug 1996 11:00:04 +0200 paulson Added le_eq_less_Suc; fixed some comments;
Mon, 19 Aug 1996 11:49:31 +0200 paulson Now less_zeroE is a Safe Elim rule
Tue, 25 Jun 1996 13:11:29 +0200 berghofe Changed argument order of nat_rec.
Fri, 21 Jun 1996 13:51:09 +0200 berghofe Replaced occurrence of fast_tac by Fast_tac .
less more (0) -60 tip