| #
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
|