| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 14:32:45 +0100 |
wenzelm |
merged, resolving some conflicts;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:56:43 +0100 |
wenzelm |
eliminated hard tabs (assuming tab-width=2);
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 10:00:53 +0100 |
haftmann |
more direct simplification rules for 1 div/mod numeral;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 21:32:41 +0100 |
blanchet |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
explicit type class for modelling even/odd parity
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
more lemmas on division
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Mon, 26 Aug 2013 11:41:17 +0200 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:35:01 +0200 |
haftmann |
spelling and typos
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
relaxed preconditions
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
type class for generic division algorithm on numerals
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
added lemma
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 19 Jun 2013 17:34:56 +0200 |
noschinl |
added lemma
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 11:40:23 +0100 |
wenzelm |
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 09:18:16 +0200 |
huffman |
add simp rules for dvd on negative numerals
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 11:16:35 +0200 |
huffman |
removed redundant nat-specific copies of theorems
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 20:19:23 +0200 |
huffman |
remove more redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:49:23 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:04:51 +0200 |
huffman |
generalized lemma zpower_zmod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:53:48 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:40:11 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:34:04 +0200 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:27:49 +0200 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 12:42:54 +0200 |
huffman |
move int::ring_div instance upward, simplify several proofs
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 11:41:16 +0200 |
huffman |
extend definition of divmod_int_rel to handle denominator=0 case
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 11:02:18 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 10:34:12 +0200 |
huffman |
shorten a proof
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 10:20:31 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 09:44:56 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 11:04:38 +0100 |
huffman |
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 15:17:03 +0100 |
bulwahn |
removing some unnecessary premises from Divides
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 14:23:46 +0100 |
huffman |
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 15:20:27 +0100 |
huffman |
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|