#
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals --HG-- extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
#
4be69ed9 |
|
22-Jun-2019 |
haftmann <none@none> |
made LaTeX happy
|
#
caa31cef |
|
22-Jun-2019 |
haftmann <none@none> |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
#
7b38a052 |
|
14-Jun-2019 |
haftmann <none@none> |
moved comment to approproiate place
|
#
af54527e |
|
14-Jun-2019 |
haftmann <none@none> |
removed outcommented example which seems not to work as advertized
|
#
699a497b |
|
13-Apr-2019 |
haftmann <none@none> |
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is --HG-- extra : rebase_source : 7ac166208fa2a49e90c60865e74188d18da004a9
|
#
a4a6b144 |
|
09-Apr-2019 |
haftmann <none@none> |
common type class for distributive division
|
#
5fc8587d |
|
04-Feb-2019 |
Manuel Eberl <eberlm@in.tum.de> |
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre) --HG-- extra : rebase_source : 29b9c3cdb252ae5f1a4a62f42d234f697238896b
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
05936fb0 |
|
23-Dec-2018 |
haftmann <none@none> |
more rules
|
#
14f1ca5d |
|
28-Jun-2018 |
wenzelm <none@none> |
avoid pending shyps in global theory facts;
|
#
a0960b42 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Generalising and renaming some basic results
|
#
8b81086d |
|
09-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Syntax for the special cases Min(A`I) and Max (A`I)
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
84c54928 |
|
27-Feb-2017 |
paulson <lp15@cam.ac.uk> |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
#
8863117a |
|
17-Dec-2016 |
haftmann <none@none> |
restructured matter on polynomials and normalized fractions --HG-- extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625
|
#
d8f09348 |
|
20-Oct-2016 |
haftmann <none@none> |
more on sgn in linear ordered fields --HG-- extra : rebase_source : eb504a9c21421694df61ac849381f6094d183dc7
|
#
049952fc |
|
18-Oct-2016 |
haftmann <none@none> |
suitable logical type class for abs, sgn --HG-- extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041
|
#
dc1c0020 |
|
28-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material connected with HOL Light measure theory, plus more rationalisation
|
#
70cb89b7 |
|
01-Mar-2016 |
haftmann <none@none> |
tuned bootstrap order to provide type classes in a more sensible order --HG-- extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9
|
#
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
|
#
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
#
c9f3da2d |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <->;
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
7f504e11 |
|
23-Sep-2015 |
paulson <lp15@cam.ac.uk> |
Useful facts about min/max, etc.
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
8ddc1a1c |
|
08-Jul-2015 |
haftmann <none@none> |
tuned facts
|
#
ca155b5f |
|
25-Jun-2015 |
haftmann <none@none> |
more theorems
|
#
a596c25e |
|
01-Jun-2015 |
haftmann <none@none> |
implicit partial divison operation in integral domains
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
#
76fd28af |
|
23-Mar-2015 |
hoelzl <none@none> |
fix parameter order of NO_MATCH
|
#
08ee2a04 |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
#
55832464 |
|
19-Feb-2015 |
haftmann <none@none> |
establish unique preferred fact names
|
#
80228203 |
|
15-Feb-2015 |
haftmann <none@none> |
times_divide_eq rules are already [simp] despite of comment
|
#
1bf80f13 |
|
14-Feb-2015 |
haftmann <none@none> |
less warnings
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
2227b563 |
|
24-Oct-2014 |
hoelzl <none@none> |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
#
b7351c6c |
|
02-Oct-2014 |
haftmann <none@none> |
moved lemmas out of Int.thy which have nothing to do with int --HG-- extra : rebase_source : a6db16c774c1c078a2ed1a129509da61fa662a39
|
#
49bf20a8 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems;
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
66804330 |
|
14-Apr-2014 |
hoelzl <none@none> |
added divide_nonneg_nonneg and co; made it a simp rule --HG-- extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47
|
#
838cbeac |
|
11-Apr-2014 |
nipkow <none@none> |
made divide_pos_pos a simp rule
|
#
654ae398 |
|
09-Apr-2014 |
hoelzl <none@none> |
add divide_simps
|
#
d749d414 |
|
09-Apr-2014 |
hoelzl <none@none> |
field_simps: better support for negation and division, and power
|
#
77b90a1d |
|
09-Apr-2014 |
hoelzl <none@none> |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
#
4dd5ee0f |
|
06-Apr-2014 |
nipkow <none@none> |
tuned lemmas: more general class
|
#
1629b0e4 |
|
06-Apr-2014 |
nipkow <none@none> |
made field_simps "more complete"
|
#
1d199f25 |
|
04-Apr-2014 |
paulson <lp15@cam.ac.uk> |
A single [simp] to handle the case -a/-b.
|
#
245904c9 |
|
04-Apr-2014 |
paulson <lp15@cam.ac.uk> |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
#
36a1e2cc |
|
03-Apr-2014 |
paulson <lp15@cam.ac.uk> |
removing simprule status for divide_minus_left and divide_minus_right
|
#
528e8580 |
|
02-Apr-2014 |
paulson <lp15@cam.ac.uk> |
New theorems for extracting quotients
|
#
0f82e936 |
|
24-Feb-2014 |
paulson <lp15@cam.ac.uk> |
A few lemmas about summations, etc.
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
efe08492 |
|
27-Aug-2013 |
hoelzl <none@none> |
renamed typeclass dense_linorder to unbounded_dense_linorder --HG-- extra : rebase_source : 1aec1d46ec989f6555ab53f40d6db74ef5536fe0
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
1530d475 |
|
03-Sep-2011 |
huffman <none@none> |
simplify proof
|
#
c6f0818a |
|
08-Aug-2011 |
huffman <none@none> |
moved division ring stuff from Rings.thy to Fields.thy
|
#
72ecf077 |
|
20-May-2011 |
hoelzl <none@none> |
add divide_.._cancel, inverse_.._iff
|
#
b39893a2 |
|
08-May-2010 |
huffman <none@none> |
add lemmas one_less_inverse and one_le_inverse
|
#
754cf751 |
|
06-May-2010 |
haftmann <none@none> |
moved some lemmas from Groebner_Basis here
|
#
31b30fca |
|
26-Apr-2010 |
haftmann <none@none> |
tuned whitespace
|
#
4c97101c |
|
27-Apr-2010 |
haftmann <none@none> |
got rid of [simplified]
|
#
b2856170 |
|
27-Apr-2010 |
haftmann <none@none> |
tuned class linordered_field_inverse_zero
|
#
756c3e6e |
|
26-Apr-2010 |
haftmann <none@none> |
use new classes (linordered_)field_inverse_zero
|
#
7e21e473 |
|
26-Apr-2010 |
haftmann <none@none> |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
#
5c5d6ac7 |
|
25-Apr-2010 |
haftmann <none@none> |
field_simps as named theorems
|
#
a2cff576 |
|
23-Apr-2010 |
haftmann <none@none> |
less special treatment of times_divide_eq [simp]
|
#
8f9b71d9 |
|
23-Apr-2010 |
haftmann <none@none> |
more localization; factored out lemmas for division_ring
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
87684496 |
|
04-Mar-2010 |
hoelzl <none@none> |
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
|
#
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
#
b033a7b7 |
|
10-Feb-2010 |
haftmann <none@none> |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
#
4fd6db3f |
|
10-Feb-2010 |
haftmann <none@none> |
moved constants inverse and divide to Ring.thy
|
#
875c5b73 |
|
08-Feb-2010 |
haftmann <none@none> |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields --HG-- rename : src/HOL/Ring_and_Field.thy => src/HOL/Fields.thy rename : src/HOL/OrderedGroup.thy => src/HOL/Groups.thy rename : src/HOL/Ring_and_Field.thy => src/HOL/Rings.thy
|