src/HOL/Divides.thy
Wed, 16 Nov 2011 15:20:27 +0100 huffman rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
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
Tue, 06 Sep 2011 19:03:41 -0700 huffman avoid using legacy theorem names
Wed, 29 Jun 2011 17:35:46 +0200 wenzelm modernized some simproc setup;
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Fri, 17 Sep 2010 16:15:33 +0200 nipkow added lemmas
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 04 May 2010 08:55:39 +0200 haftmann a ring_div is a ring_1_no_zero_divisors
Wed, 17 Mar 2010 19:55:07 +0100 boehmes tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
Tue, 09 Mar 2010 15:47:15 +0100 haftmann weakend class ring_div; tuned
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Wed, 24 Feb 2010 14:19:53 +0100 haftmann lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Tue, 02 Feb 2010 11:38:38 +0100 blanchet added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
Sat, 02 Jan 2010 21:31:15 +0100 nipkow removed legacy asm_lr
Fri, 18 Dec 2009 12:00:29 +0100 blanchet polished Nitpick's binary integer support etc.;
Fri, 20 Nov 2009 07:23:36 +0100 nipkow added lemma
Tue, 17 Nov 2009 11:10:22 +0000 webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
Tue, 17 Nov 2009 10:17:53 +0000 webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
Fri, 30 Oct 2009 18:32:40 +0100 haftmann tuned code setup
Fri, 30 Oct 2009 14:00:43 +0100 haftmann combined former theories Divides and IntDiv to one theory Divides
Thu, 29 Oct 2009 22:13:09 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Wed, 28 Oct 2009 19:09:47 +0100 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
Wed, 28 Oct 2009 17:44:03 +0100 haftmann moved lemmas for dvd on nat to theories Nat and Power
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Tue, 07 Jul 2009 17:39:51 +0200 nipkow renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
Mon, 15 Jun 2009 21:29:04 -0700 huffman generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
Mon, 15 Jun 2009 17:59:36 -0700 huffman move lemma div_power into semiring_div context; class ring_div inherits from idom
Tue, 28 Apr 2009 13:34:45 +0200 haftmann dropped reference to class recpower and lemma duplicate
Thu, 16 Apr 2009 14:02:11 +0200 haftmann tuned setups of CancelDivMod
Thu, 16 Apr 2009 10:11:34 +0200 haftmann tightended specification of class semiring_div
Wed, 15 Apr 2009 15:30:37 +0200 haftmann more coherent developement in Divides.thy and IntDiv.thy
Wed, 01 Apr 2009 18:41:15 +0200 nipkow added nat_div_gt_0 [simp]
Wed, 01 Apr 2009 16:03:00 +0200 nipkow added strong_setprod_cong[cong] (in analogy with setsum)
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Sun, 22 Mar 2009 20:46:11 +0100 haftmann lemma nat_dvd_not_less moved here from Arith_Tools
Thu, 12 Mar 2009 23:01:25 +0100 haftmann merged
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
Thu, 12 Mar 2009 15:31:26 +0100 nipkow added div lemmas
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 17:05:18 +0100 nipkow removed and renamed redundant lemmas
Sun, 01 Mar 2009 10:24:57 +0100 nipkow added lemmas by Jeremy Avigad
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
Mon, 23 Feb 2009 13:55:36 -0800 huffman move lemma dvd_mod_imp_dvd into class semiring_div
Sun, 22 Feb 2009 11:30:41 +0100 nipkow added dvd_div_mult
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Fri, 20 Feb 2009 20:50:49 +0100 nipkow removed subsumed lemmas
Wed, 18 Feb 2009 10:24:48 -0800 huffman generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Sun, 15 Feb 2009 22:58:02 +0100 nipkow dvd and setprod lemmas
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation
Thu, 08 Jan 2009 09:12:29 -0800 huffman add class ring_div; generalize mod/diff/minus proofs for class ring_div
less more (0) -100 -60 tip