| 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
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 16:15:33 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:39 +0200 |
haftmann |
a ring_div is a ring_1_no_zero_divisors
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 15:47:15 +0100 |
haftmann |
weakend class ring_div; tuned
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:58 +0100 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:19:53 +0100 |
haftmann |
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|