src/HOL/Nat.thy
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Thu, 26 Feb 2009 08:44:12 -0800 huffman revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
Wed, 25 Feb 2009 06:53:15 -0800 huffman add lemma diff_Suc_1
Mon, 23 Feb 2009 16:25:52 -0800 huffman make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
Sun, 22 Feb 2009 17:25:28 +0100 nipkow added lemmas
Thu, 12 Feb 2009 18:14:43 +0100 nipkow Moved FTA into Lib and cleaned it up a little.
Tue, 10 Feb 2009 09:58:58 +0000 paulson merged
Tue, 10 Feb 2009 09:46:11 +0000 paulson Deleted the induction rule nat_induct2, which was too weak and not used even once.
Mon, 09 Feb 2009 18:50:10 +0100 nipkow new attribute "arith" for facts supplied to arith.
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 28 Jan 2009 11:02:12 +0100 haftmann nat is a bot instance
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 07 Oct 2008 16:07:18 +0200 haftmann tuned of_nat code generation
Mon, 11 Aug 2008 14:49:53 +0200 haftmann moved class wellorder to theory Orderings
Fri, 08 Aug 2008 09:26:15 +0200 nipkow added lemmas
Fri, 25 Jul 2008 12:03:28 +0200 haftmann tuned
Thu, 17 Jul 2008 15:21:52 +0200 krauss simplified proofs
Thu, 17 Jul 2008 13:50:17 +0200 nipkow added lemmas
Sat, 14 Jun 2008 23:20:05 +0200 wenzelm removed obsolete nat_induct_tac -- cannot work without;
Tue, 10 Jun 2008 19:15:21 +0200 wenzelm added nat_induct_tac (works without context);
Tue, 10 Jun 2008 15:30:33 +0200 haftmann rep_datatype command now takes list of constructors as input arguments
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Wed, 19 Mar 2008 18:15:25 +0100 wenzelm removed redundant Nat.less_not_sym, Nat.less_asym;
Tue, 18 Mar 2008 20:33:29 +0100 wenzelm removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
Mon, 17 Mar 2008 18:37:00 +0100 wenzelm removed duplicate lemmas;
Tue, 26 Feb 2008 20:38:14 +0100 haftmann tuned heading
Tue, 26 Feb 2008 11:18:43 +0100 bulwahn Added useful general lemmas from the work with the HeapMonad
Wed, 20 Feb 2008 14:52:38 +0100 haftmann tuned structures in arith_data.ML
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
less more (0) -100 -60 tip