| 2015-06-01 |
haftmann |
2015-06-01 |
implicit partial divison operation in integral domains
|
file | diff | annotate |
| 2015-06-01 |
haftmann |
2015-06-01 |
separate class for division operator, with particular syntax added in more specific classes
|
file | diff | annotate |
| 2015-03-31 |
haftmann |
2015-03-31 |
given up separate type classes demanding `inverse 0 = 0`
|
file | diff | annotate |
| 2015-03-23 |
hoelzl |
2015-03-23 |
fix parameter order of NO_MATCH
|
file | diff | annotate |
| 2015-03-10 |
paulson |
2015-03-10 |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file | diff | annotate |
| 2015-02-19 |
haftmann |
2015-02-19 |
establish unique preferred fact names
|
file | diff | annotate |
| 2015-02-15 |
haftmann |
2015-02-15 |
times_divide_eq rules are already [simp] despite of comment
|
file | diff | annotate |
| 2015-02-14 |
haftmann |
2015-02-14 |
less warnings
|
file | diff | annotate |
| 2014-11-02 |
wenzelm |
2014-11-02 |
modernized header uniformly as section;
|
file | diff | annotate |
| 2014-10-29 |
wenzelm |
2014-10-29 |
modernized setup;
|
file | diff | annotate |
| 2014-10-24 |
hoelzl |
2014-10-24 |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file | diff | annotate |
| 2014-10-02 |
haftmann |
2014-10-02 |
moved lemmas out of Int.thy which have nothing to do with int
|
file | diff | annotate |
| 2014-08-16 |
wenzelm |
2014-08-16 |
updated to named_theorems;
|
file | diff | annotate |
| 2014-07-05 |
haftmann |
2014-07-05 |
prefer ac_simps collections over separate name bindings for add and mult
|
file | diff | annotate |
| 2014-07-04 |
haftmann |
2014-07-04 |
reduced name variants for assoc and commute on plus and mult
|
file | diff | annotate |
| 2014-04-14 |
hoelzl |
2014-04-14 |
added divide_nonneg_nonneg and co; made it a simp rule
|
file | diff | annotate |
| 2014-04-11 |
nipkow |
2014-04-11 |
made divide_pos_pos a simp rule
|
file | diff | annotate |
| 2014-04-09 |
hoelzl |
2014-04-09 |
add divide_simps
|
file | diff | annotate |
| 2014-04-09 |
hoelzl |
2014-04-09 |
field_simps: better support for negation and division, and power
|
file | diff | annotate |
| 2014-04-09 |
hoelzl |
2014-04-09 |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file | diff | annotate |
| 2014-04-06 |
nipkow |
2014-04-06 |
tuned lemmas: more general class
|
file | diff | annotate |
| 2014-04-06 |
nipkow |
2014-04-06 |
made field_simps "more complete"
|
file | diff | annotate |
| 2014-04-05 |
paulson |
2014-04-05 |
A single [simp] to handle the case -a/-b.
|
file | diff | annotate |
| 2014-04-04 |
paulson |
2014-04-04 |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file | diff | annotate |
| 2014-04-03 |
paulson |
2014-04-03 |
removing simprule status for divide_minus_left and divide_minus_right
|
file | diff | annotate |
| 2014-04-02 |
paulson |
2014-04-02 |
New theorems for extracting quotients
|
file | diff | annotate |
| 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 |