src/HOL/NatDef.ML
Thu, 05 Feb 1998 10:46:31 +0100 paulson New max, min theorems
Thu, 08 Jan 1998 18:09:07 +0100 oheimb added select_equality to the implicit claset
Tue, 23 Dec 1997 11:40:47 +0100 paulson tidied
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort;
Wed, 03 Dec 1997 17:25:43 +0100 nipkow Replaced n ~= 0 by 0 < n
Wed, 05 Nov 1997 13:23:46 +0100 paulson Ran expandshort, especially to introduce Safe_tac
Mon, 03 Nov 1997 21:12:21 +0100 wenzelm nat datatype_info moved to Nat.thy;
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Thu, 30 Oct 1997 09:45:03 +0100 nipkow For each datatype `t' there is now a theorem `split_t_case' of the form
Fri, 24 Oct 1997 17:25:33 +0200 wenzelm ProtoPure.flexpair_def;
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Wed, 01 Oct 1997 18:13:41 +0200 wenzelm fully qualified names: Theory.add_XXX;
Fri, 26 Sep 1997 10:21:14 +0200 paulson Minor tidying to use Clarify_tac, etc.
Wed, 23 Jul 1997 11:50:26 +0200 paulson Uses new version of Datatype.occs_in_prems
Wed, 02 Jul 1997 11:59:10 +0200 nipkow Added the following lemmas tp Divides and a few others to Arith and NatDef:
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort
Fri, 30 May 1997 15:30:52 +0200 paulson Moved "less_eq" to NatDef from Arith
Tue, 27 May 1997 13:23:53 +0200 paulson New theorem le_Suc_eq
Mon, 26 May 1997 12:39:57 +0200 paulson Renamed lessD to Suc_leI
Fri, 23 May 1997 09:17:26 +0200 nipkow Added overloaded function `size' for all datatypes.
Thu, 22 May 1997 13:05:52 +0200 nipkow Added rotation to exhaust_tac.
Thu, 22 May 1997 09:20:28 +0200 nipkow Added exhaustion thm and exhaust_tac for each datatype.
Tue, 20 May 1997 11:39:32 +0200 paulson New pattern-matching definition of pred_nat
Thu, 08 May 1997 11:44:59 +0200 nipkow Modified def of Least, which, as Markus correctly complained, looked like
Wed, 30 Apr 1997 13:39:56 +0200 paulson Fixed clasets so that blast_tac would work
Thu, 24 Apr 1997 18:06:46 +0200 nipkow Introduced a generic "induct_tac" which picks up the right induction scheme
Wed, 23 Apr 1997 11:18:29 +0200 paulson Ran expandshort
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac
Tue, 04 Mar 1997 10:48:36 +0100 paulson Renamed constant "not" to "Not"
Tue, 25 Feb 1997 15:05:14 +0100 pusch function nat_add_primrec added to allow primrec definitions over nat
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes.
less more (0) tip