| 2022-08-19 |
haftmann |
more thorough split rules for div and mod on numerals, tuned split rules setup
|
file |
diff |
annotate
|
| 2022-08-19 |
haftmann |
consolidated attribute name
|
file |
diff |
annotate
|
| 2022-07-22 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| 2021-03-11 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| 2020-04-05 |
paulson |
Tidied up more ancient, horrible proofs. Liberalised frac_le
|
file |
diff |
annotate
|
| 2019-10-09 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| 2019-06-22 |
haftmann |
made LaTeX happy
|
file |
diff |
annotate
|
| 2019-06-22 |
haftmann |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
file |
diff |
annotate
|
| 2019-06-14 |
haftmann |
moved comment to approproiate place
|
file |
diff |
annotate
|
| 2019-06-14 |
haftmann |
removed outcommented example which seems not to work as advertized
|
file |
diff |
annotate
|
| 2019-04-13 |
haftmann |
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
|
file |
diff |
annotate
|
| 2019-04-09 |
haftmann |
common type class for distributive division
|
file |
diff |
annotate
|
| 2019-02-04 |
Manuel Eberl |
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
|
file |
diff |
annotate
|
| 2019-01-06 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| 2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 2018-12-23 |
haftmann |
more rules
|
file |
diff |
annotate
|
| 2018-06-29 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 2018-06-28 |
wenzelm |
avoid pending shyps in global theory facts;
|
file |
diff |
annotate
|
| 2018-06-28 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| 2018-04-09 |
paulson |
Syntax for the special cases Min(A`I) and Max (A`I)
|
file |
diff |
annotate
|
| 2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2017-02-27 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
file |
diff |
annotate
|
| 2016-12-17 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| 2016-10-20 |
haftmann |
more on sgn in linear ordered fields
|
file |
diff |
annotate
|
| 2016-10-18 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| 2016-09-28 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
| 2016-03-01 |
haftmann |
tuned bootstrap order to provide type classes in a more sensible order
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| 2015-12-28 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| 2015-12-27 |
wenzelm |
discontinued ASCII replacement syntax <->;
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-09-23 |
paulson |
Useful facts about min/max, etc.
|
file |
diff |
annotate
|
| 2015-09-01 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
tuned facts
|
file |
diff |
annotate
|
| 2015-06-25 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| 2015-06-01 |
haftmann |
implicit partial divison operation in integral domains
|
file |
diff |
annotate
|
| 2015-06-01 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| 2015-03-31 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| 2015-03-23 |
hoelzl |
fix parameter order of NO_MATCH
|
file |
diff |
annotate
|
| 2015-03-10 |
paulson |
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 |
establish unique preferred fact names
|
file |
diff |
annotate
|
| 2015-02-15 |
haftmann |
times_divide_eq rules are already [simp] despite of comment
|
file |
diff |
annotate
|
| 2015-02-14 |
haftmann |
less warnings
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-10-29 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| 2014-10-24 |
hoelzl |
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 |
moved lemmas out of Int.thy which have nothing to do with int
|
file |
diff |
annotate
|
| 2014-08-16 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| 2014-07-05 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| 2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| 2014-04-14 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| 2014-04-11 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| 2014-04-09 |
hoelzl |
add divide_simps
|
file |
diff |
annotate
|
| 2014-04-09 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| 2014-04-09 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| 2014-04-06 |
nipkow |
tuned lemmas: more general class
|
file |
diff |
annotate
|
| 2014-04-06 |
nipkow |
made field_simps "more complete"
|
file |
diff |
annotate
|
| 2014-04-05 |
paulson |
A single [simp] to handle the case -a/-b.
|
file |
diff |
annotate
|
| 2014-04-04 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file |
diff |
annotate
|