| 2014-02-24 |
paulson |
2014-02-24 |
A few lemmas about summations, etc.
|
file | diff | annotate |
| 2013-11-01 |
haftmann |
2013-11-01 |
more simplification rules on unary and binary minus
|
file | diff | annotate |
| 2013-10-18 |
blanchet |
2013-10-18 |
killed most "no_atp", to make Sledgehammer more complete
|
file | diff | annotate |
| 2013-09-03 |
wenzelm |
2013-09-03 |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file | diff | annotate |
| 2013-08-27 |
hoelzl |
2013-08-27 |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file | diff | annotate |
| 2013-06-23 |
haftmann |
2013-06-23 |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file | diff | annotate |
| 2011-09-13 |
huffman |
2011-09-13 |
tuned proofs
|
file | diff | annotate |
| 2011-09-03 |
huffman |
2011-09-03 |
simplify proof
|
file | diff | annotate |
| 2011-08-08 |
huffman |
2011-08-08 |
moved division ring stuff from Rings.thy to Fields.thy
|
file | diff | annotate |
| 2011-05-20 |
hoelzl |
2011-05-20 |
add divide_.._cancel, inverse_.._iff
|
file | diff | annotate |
| 2010-05-08 |
huffman |
2010-05-08 |
add lemmas one_less_inverse and one_le_inverse
|
file | diff | annotate |
| 2010-05-06 |
haftmann |
2010-05-06 |
moved some lemmas from Groebner_Basis here
|
file | diff | annotate |
| 2010-04-27 |
haftmann |
2010-04-27 |
tuned whitespace
|
file | diff | annotate |
| 2010-04-27 |
haftmann |
2010-04-27 |
got rid of [simplified]
|
file | diff | annotate |
| 2010-04-27 |
haftmann |
2010-04-27 |
tuned class linordered_field_inverse_zero
|
file | diff | annotate |
| 2010-04-26 |
haftmann |
2010-04-26 |
use new classes (linordered_)field_inverse_zero
|
file | diff | annotate |
| 2010-04-26 |
haftmann |
2010-04-26 |
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-25 |
haftmann |
2010-04-25 |
field_simps as named theorems
|
file | diff | annotate |
| 2010-04-23 |
haftmann |
2010-04-23 |
less special treatment of times_divide_eq [simp]
|
file | diff | annotate |
| 2010-04-23 |
haftmann |
2010-04-23 |
more localization; factored out lemmas for division_ring
|
file | diff | annotate |
| 2010-03-18 |
blanchet |
2010-03-18 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| 2010-03-04 |
hoelzl |
2010-03-04 |
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
|
file | diff | annotate |
| 2010-02-18 |
huffman |
2010-02-18 |
get rid of many duplicate simp rule warnings
|
file | diff | annotate |
| 2010-02-10 |
haftmann |
2010-02-10 |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
file | diff | annotate |
| 2010-02-10 |
haftmann |
2010-02-10 |
moved constants inverse and divide to Ring.thy
|
file | diff | annotate |
| 2010-02-08 |
haftmann |
2010-02-08 |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file | diff | annotate | base |