src/HOL/NatDef.ML
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