src/HOL/Nat.thy
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
Fri, 30 Mar 2012 08:11:52 +0200 huffman move lemmas from Nat_Numeral.thy to Nat.thy
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sat, 28 Jan 2012 10:35:52 +0100 bulwahn adding yet another induction rule on natural numbers
Sat, 28 Jan 2012 10:22:46 +0100 bulwahn moving declarations back to the section they seem to belong to (cf. afffe1f72143)
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Sat, 24 Dec 2011 15:53:09 +0100 haftmann generalized type signature to permit overloading on `set`
Mon, 19 Dec 2011 14:41:08 +0100 noschinl add lemmas
Mon, 19 Dec 2011 14:41:08 +0100 noschinl weaken preconditions on lemmas
Tue, 13 Dec 2011 16:14:41 +0100 nipkow lemmas about Kleene iteration
Wed, 30 Nov 2011 18:07:14 +0100 wenzelm prefer typedef without alternative name;
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 08 Sep 2011 18:47:23 -0700 huffman remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
Wed, 07 Sep 2011 23:07:16 +0200 haftmann lemmas about +, *, min, max on nat
Sat, 20 Aug 2011 01:39:27 +0200 haftmann more uniform formatting of specifications
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Wed, 29 Jun 2011 18:12:34 +0200 wenzelm modernized some simproc setup;
Thu, 30 Sep 2010 08:50:45 +0200 haftmann tuned
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 20 Aug 2010 17:46:56 +0200 haftmann more concise characterization of of_nat operation and class semiring_char_0
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 14 Jun 2010 16:00:46 +0200 haftmann added lemma funpow_mult
Tue, 08 Jun 2010 16:37:19 +0200 haftmann qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Sun, 07 Mar 2010 07:42:46 -0800 huffman add lemmas Nats_cases and Nats_induct
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Fri, 12 Feb 2010 14:28:01 +0100 haftmann tuned import order
Tue, 09 Feb 2010 11:47:47 +0100 haftmann hide fact names clashing with fact names from Group.thy
Mon, 08 Feb 2010 17:12:27 +0100 haftmann hide fact Nat.add_0_right; make add_0_right from Groups priority
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Wed, 30 Dec 2009 01:08:33 +0100 krauss more regular axiom of infinity, with no (indirect) reference to overloaded constants
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Fri, 30 Oct 2009 18:32:40 +0100 haftmann tuned code setup
Wed, 28 Oct 2009 17:44:03 +0100 haftmann moved lemmas for dvd on nat to theories Nat and Power
Wed, 30 Sep 2009 08:21:53 +0200 haftmann tuned whitespace
Mon, 31 Aug 2009 14:09:42 +0200 nipkow tuned the simp rules for Int involving insert and intervals.
Fri, 28 Aug 2009 19:15:59 +0200 nipkow tuned proofs
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.
less more (0) -100 -60 tip