2011-12-29 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
2011-11-20 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
2011-11-16 |
huffman |
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
|
file |
diff |
annotate
|
2011-10-21 |
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
|
2011-09-12 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
2011-09-07 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
2011-06-29 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
2011-02-21 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
2011-01-14 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
2010-09-17 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
2010-08-25 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
2010-07-12 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
2010-05-04 |
haftmann |
a ring_div is a ring_1_no_zero_divisors
|
file |
diff |
annotate
|
2010-03-17 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
2010-03-09 |
haftmann |
weakend class ring_div; tuned
|
file |
diff |
annotate
|
2010-03-08 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
2010-02-24 |
haftmann |
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
|
file |
diff |
annotate
|
2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
2010-02-08 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
2010-02-02 |
blanchet |
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
|
file |
diff |
annotate
|
2010-01-02 |
nipkow |
removed legacy asm_lr
|
file |
diff |
annotate
|
2009-12-18 |
blanchet |
polished Nitpick's binary integer support etc.;
|
file |
diff |
annotate
|
2009-11-20 |
nipkow |
added lemma
|
file |
diff |
annotate
|
2009-11-17 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
file |
diff |
annotate
|
2009-11-17 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
file |
diff |
annotate
|
2009-10-30 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
2009-10-30 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
2009-10-29 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
2009-10-29 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
2009-10-28 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
2009-10-28 |
haftmann |
moved lemmas for dvd on nat to theories Nat and Power
|
file |
diff |
annotate
|
2009-07-15 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2009-07-14 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
2009-07-07 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
file |
diff |
annotate
|
2009-06-16 |
huffman |
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
|
file |
diff |
annotate
|
2009-06-16 |
huffman |
move lemma div_power into semiring_div context; class ring_div inherits from idom
|
file |
diff |
annotate
|
2009-04-28 |
haftmann |
dropped reference to class recpower and lemma duplicate
|
file |
diff |
annotate
|
2009-04-16 |
haftmann |
tuned setups of CancelDivMod
|
file |
diff |
annotate
|
2009-04-16 |
haftmann |
tightended specification of class semiring_div
|
file |
diff |
annotate
|
2009-04-15 |
haftmann |
more coherent developement in Divides.thy and IntDiv.thy
|
file |
diff |
annotate
|
2009-04-01 |
nipkow |
added nat_div_gt_0 [simp]
|
file |
diff |
annotate
|
2009-04-01 |
nipkow |
added strong_setprod_cong[cong] (in analogy with setsum)
|
file |
diff |
annotate
|
2009-03-26 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
2009-03-22 |
haftmann |
lemma nat_dvd_not_less moved here from Arith_Tools
|
file |
diff |
annotate
|
2009-03-12 |
haftmann |
merged
|
file |
diff |
annotate
|
2009-03-12 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
2009-03-12 |
nipkow |
added div lemmas
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-03-03 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
2009-03-01 |
nipkow |
added lemmas by Jeremy Avigad
|
file |
diff |
annotate
|
2009-02-24 |
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
|
file |
diff |
annotate
|
2009-02-23 |
huffman |
move lemma dvd_mod_imp_dvd into class semiring_div
|
file |
diff |
annotate
|
2009-02-22 |
nipkow |
added dvd_div_mult
|
file |
diff |
annotate
|
2009-02-21 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
2009-02-20 |
nipkow |
removed subsumed lemmas
|
file |
diff |
annotate
|
2009-02-18 |
huffman |
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
|
file |
diff |
annotate
|
2009-02-17 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
2009-02-15 |
nipkow |
dvd and setprod lemmas
|
file |
diff |
annotate
|
2009-01-28 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|