src/HOL/Nat.thy
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Thu, 18 Jun 2009 19:54:21 +0200 krauss generalized less_Suc_induct
Thu, 14 May 2009 15:09:47 +0200 haftmann monomorphic code generation for power operations
Mon, 11 May 2009 15:18:32 +0200 haftmann tuned interface of Lin_Arith
Wed, 29 Apr 2009 17:15:01 -0700 huffman reimplement reorientation simproc using theory data
Fri, 24 Apr 2009 18:20:37 +0200 haftmann some jokes are just too bad to appear in a theory file
Fri, 24 Apr 2009 17:45:15 +0200 haftmann funpow and relpow with shared "^^" syntax
Thu, 23 Apr 2009 12:17:50 +0200 haftmann avoid local [code]
Mon, 20 Apr 2009 09:32:40 +0200 haftmann power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
Mon, 23 Mar 2009 19:01:16 +0100 haftmann moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
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
less more (0) -100 -60 tip