src/HOL/Nat.thy
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.
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
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!)
less more (0) -120 tip