src/HOL/Divides.thy
Sun, 18 Aug 2013 15:29:50 +0200 haftmann added lemma
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Wed, 19 Jun 2013 17:34:56 +0200 noschinl added lemma
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 28 Feb 2013 11:40:23 +0100 wenzelm proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
Sun, 17 Feb 2013 21:29:30 +0100 haftmann Sieve of Eratosthenes
Fri, 07 Dec 2012 16:25:33 +0100 wenzelm avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Fri, 27 Jul 2012 19:27:21 +0200 huffman move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
Mon, 02 Apr 2012 09:18:16 +0200 huffman add simp rules for dvd on negative numerals
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
Fri, 30 Mar 2012 11:16:35 +0200 huffman removed redundant nat-specific copies of theorems
Tue, 27 Mar 2012 20:19:23 +0200 huffman remove more redundant lemmas
Tue, 27 Mar 2012 16:49:23 +0200 huffman tuned proofs
Tue, 27 Mar 2012 19:21:05 +0200 huffman remove redundant lemmas
Tue, 27 Mar 2012 16:04:51 +0200 huffman generalized lemma zpower_zmod
Tue, 27 Mar 2012 15:53:48 +0200 huffman remove redundant lemma
Tue, 27 Mar 2012 15:40:11 +0200 huffman remove redundant lemma
Tue, 27 Mar 2012 15:34:04 +0200 huffman generalize more div/mod lemmas
Tue, 27 Mar 2012 15:27:49 +0200 huffman generalize some theorems about div/mod
Tue, 27 Mar 2012 14:49:56 +0200 huffman remove redundant lemmas
Tue, 27 Mar 2012 12:42:54 +0200 huffman move int::ring_div instance upward, simplify several proofs
Tue, 27 Mar 2012 11:45:02 +0200 huffman rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
Tue, 27 Mar 2012 11:41:16 +0200 huffman extend definition of divmod_int_rel to handle denominator=0 case
Tue, 27 Mar 2012 11:02:18 +0200 huffman tuned proofs
Tue, 27 Mar 2012 10:34:12 +0200 huffman shorten a proof
Tue, 27 Mar 2012 10:20:31 +0200 huffman simplify some proofs
Tue, 27 Mar 2012 09:54:39 +0200 huffman rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
Tue, 27 Mar 2012 09:44:56 +0200 huffman simplify some proofs
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 21 Feb 2012 11:04:38 +0100 huffman remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
Mon, 20 Feb 2012 15:17:03 +0100 bulwahn removing some unnecessary premises from Divides
Mon, 20 Feb 2012 14:23:46 +0100 huffman simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
Thu, 29 Dec 2011 10:47:54 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
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
less more (0) -100 -60 tip