src/HOL/Nat.thy
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Mon, 21 Jan 2008 08:43:27 +0100 haftmann tuned code setup
Tue, 18 Dec 2007 12:26:24 +0100 berghofe Renamed *.size to prod.size.
Thu, 13 Dec 2007 07:09:00 +0100 haftmann added lemma
Fri, 07 Dec 2007 15:07:59 +0100 haftmann instantiation target rather than legacy instance
Thu, 06 Dec 2007 17:05:44 +0100 haftmann temporary code generator work arounds
Thu, 06 Dec 2007 16:36:19 +0100 haftmann authentic primrec
Wed, 05 Dec 2007 14:15:45 +0100 haftmann simplified infrastructure for code generator operational equality
Fri, 30 Nov 2007 20:13:03 +0100 haftmann adjustions to due to instance target
Thu, 29 Nov 2007 17:08:26 +0100 haftmann instance command as rudimentary class target
Wed, 28 Nov 2007 09:01:37 +0100 haftmann dropped implicit assumption proof
Sat, 10 Nov 2007 23:03:52 +0100 wenzelm tuned specifications of 'notation';
Tue, 30 Oct 2007 08:45:55 +0100 haftmann simplified proof
Thu, 25 Oct 2007 19:27:50 +0200 haftmann various localizations
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Tue, 23 Oct 2007 13:10:19 +0200 paulson random tidying of proofs
Mon, 22 Oct 2007 16:54:50 +0200 haftmann dropped superfluous inlining lemmas
Sun, 21 Oct 2007 22:33:35 +0200 nipkow More changes from >0 to ~=0::nat
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:30 +0200 chaieb neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
Thu, 18 Oct 2007 09:20:55 +0200 haftmann localized mono predicate
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax
Fri, 12 Oct 2007 08:25:47 +0200 haftmann refined; moved class power to theory Power
Wed, 26 Sep 2007 20:27:57 +0200 haftmann added code lemma for 1
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Mon, 03 Sep 2007 10:00:24 +0200 nipkow added variations on infinite descent
Mon, 27 Aug 2007 14:19:38 +0200 nipkow Added infinite_descent
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Thu, 09 Aug 2007 15:52:47 +0200 haftmann localized of_nat
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Tue, 31 Jul 2007 19:40:22 +0200 wenzelm added Tools/lin_arith.ML;
Tue, 31 Jul 2007 00:56:26 +0200 wenzelm arith method setup: proper context;
Thu, 19 Jul 2007 21:47:37 +0200 haftmann moved set Nats to Nat.thy
Wed, 11 Jul 2007 11:04:39 +0200 berghofe Adapted to new package for inductive sets.
Fri, 22 Jun 2007 22:41:17 +0200 huffman fix looping simp rule
Wed, 20 Jun 2007 17:28:55 +0200 huffman remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
Wed, 20 Jun 2007 05:18:39 +0200 huffman change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
Tue, 12 Jun 2007 23:14:29 +0200 huffman add lemma inj_of_nat
Wed, 06 Jun 2007 20:49:04 +0200 huffman add axclass semiring_char_0 for types where of_nat is injective
Wed, 06 Jun 2007 17:00:09 +0200 huffman generalize of_nat and related constants to class semiring_1
Tue, 05 Jun 2007 19:23:09 +0200 haftmann tuned boostrap
Thu, 17 May 2007 22:58:53 +0200 krauss added induction principles for induction "backwards": P (Suc n) ==> P n
Thu, 10 May 2007 10:21:50 +0200 haftmann size [nat] is identity
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Tue, 17 Apr 2007 00:30:44 +0200 wenzelm tuned proofs;
Tue, 20 Mar 2007 15:52:40 +0100 haftmann added instance for lattice
Tue, 20 Mar 2007 08:27:15 +0100 haftmann explizit "type" superclass
Fri, 23 Feb 2007 08:39:21 +0100 haftmann adjusted code lemmas
Wed, 14 Feb 2007 10:06:14 +0100 haftmann simpliefied instance statement
Wed, 07 Feb 2007 17:28:09 +0100 berghofe Adapted to new inductive definition package.
Fri, 26 Jan 2007 10:24:33 +0100 paulson min/max lemmas (actually unused!)
Mon, 22 Jan 2007 15:08:48 +0100 krauss Added lemma nat_size[simp]: "size (n::nat) = n"
Wed, 06 Dec 2006 01:12:43 +0100 wenzelm added aliases for nat_recs/cases;
Wed, 22 Nov 2006 10:20:16 +0100 haftmann cleanup
Sat, 18 Nov 2006 00:20:18 +0100 haftmann power is now a class
Wed, 08 Nov 2006 21:45:13 +0100 wenzelm removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
Mon, 06 Nov 2006 16:28:31 +0100 haftmann code generator module naming improved
Mon, 16 Oct 2006 14:07:19 +0200 haftmann added explicit print translation for nat_case
less more (0) -100 -60 tip