| #
95154910 |
|
27-Apr-2019 |
paulson <lp15@cam.ac.uk> |
some variable renaming
|
| #
d378eddf |
|
27-Apr-2019 |
paulson <lp15@cam.ac.uk> |
tweaks esp renaming Rep_preal
|
| #
58916f93 |
|
27-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Massive restructuring; deleting unused theorems
|
| #
399fc6bd |
|
26-Apr-2019 |
paulson <lp15@cam.ac.uk> |
partial updating to eliminate ASCII style and some applys
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
51f16e42 |
|
27-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
36e39dcf |
|
26-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
| #
ee8e8234 |
|
06-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
603f8dfb |
|
12-Jun-2015 |
haftmann <none@none> |
uniform _ div _ as infix syntax for ring division
--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9
|
| #
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`
|
| #
c41b64c5 |
|
23-Mar-2015 |
haftmann <none@none> |
explicit commutative additive inverse operation;
more explicit focal point for commutative monoids with an inverse operation
--HG--
extra : rebase_source : ed4c155428dd5783c8e0663805a92b15992e85d3
|
| #
e2e09bbd |
|
23-Mar-2015 |
haftmann <none@none> |
modernized
--HG--
extra : rebase_source : 2c4db3bfcc2dc5aeb63886b4c52ee7765882ab5f
|
| #
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
|
| #
9fd71573 |
|
10-Jun-2014 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
Hypsubst preserves equality hypotheses
Fixes included for various theories affected by this change.
--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0
|
| #
5723122d |
|
12-Apr-2014 |
nipkow <none@none> |
made mult_pos_pos a simp rule
|
| #
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
| #
839a96d8 |
|
05-Nov-2013 |
hoelzl <none@none> |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
--HG--
rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy
|
| #
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus
--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
| #
2072947f |
|
02-Sep-2013 |
wenzelm <none@none> |
proper imports;
tuned proofs;
|
| #
efe08492 |
|
27-Aug-2013 |
hoelzl <none@none> |
renamed typeclass dense_linorder to unbounded_dense_linorder
--HG--
extra : rebase_source : 1aec1d46ec989f6555ab53f40d6db74ef5536fe0
|
| #
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
| #
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
95291102 |
|
13-Mar-2012 |
wenzelm <none@none> |
prefer abs_def over def_raw;
|
| #
d8e74f87 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without extra definition and alternative name;
tuned proofs;
|
| #
ad3ab16f |
|
13-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
tuned proofs;
|
| #
376e1c09 |
|
30-Nov-2010 |
haftmann <none@none> |
adaptions to changes in Equiv_Relation.thy
|
| #
0bb01cdc |
|
01-Oct-2010 |
haftmann <none@none> |
constant `contents` renamed to `the_elem`
|
| #
55a5de32 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
| #
66151938 |
|
08-Jun-2010 |
haftmann <none@none> |
tuned quotes, antiquotations and whitespace
|
| #
9ff567a1 |
|
10-May-2010 |
huffman <none@none> |
add more credits to ex/Dedekind_Real.thy
|
| #
97b9dc68 |
|
10-May-2010 |
huffman <none@none> |
put construction of reals using Dedekind cuts in HOL/ex
|