| 2013-12-09 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| 2013-11-04 |
haftmann |
fact generalization and name consolidation
|
file |
diff |
annotate
|
| 2013-11-01 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| 2013-10-31 |
haftmann |
generalized of_bool conversion
|
file |
diff |
annotate
|
| 2013-10-18 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| 2013-06-23 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| 2013-03-26 |
hoelzl |
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
|
file |
diff |
annotate
|
| 2012-12-07 |
nipkow |
corrected nonsensical associativity of `` and dvd
|
file |
diff |
annotate
|
| 2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| 2011-09-14 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| 2011-08-20 |
huffman |
replace lemma realpow_two_diff with new lemma square_diff_square_factored
|
file |
diff |
annotate
|
| 2011-08-20 |
huffman |
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
|
file |
diff |
annotate
|
| 2011-08-08 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| 2010-08-23 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| 2010-07-12 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| 2010-05-18 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
file |
diff |
annotate
|
| 2010-05-17 |
huffman |
remove simp attribute from square_eq_1_iff
|
file |
diff |
annotate
|
| 2010-05-11 |
huffman |
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| 2010-04-20 |
hoelzl |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
file |
diff |
annotate
|
| 2010-04-26 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
file |
diff |
annotate
|
| 2010-04-23 |
haftmann |
less special treatment of times_divide_eq [simp]
|
file |
diff |
annotate
|
| 2010-04-23 |
haftmann |
more localization; factored out lemmas for division_ring
|
file |
diff |
annotate
|
| 2010-03-18 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| 2010-03-07 |
huffman |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
file |
diff |
annotate
|
| 2010-02-22 |
haftmann |
tuned text
|
file |
diff |
annotate
|
| 2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
dropped last occurence of the linlinordered accident
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
division ring assumes divide_inverse
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
| base
|