| #
9736bb42 |
|
10-Jul-2018 |
nipkow <none@none> |
moved lemmas
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
833172d4 |
|
22-Jan-2018 |
nipkow <none@none> |
removed duplicate
|
| #
68c8f77f |
|
19-Jan-2018 |
nipkow <none@none> |
moved from AFP/Gromov
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
db0764a6 |
|
12-Apr-2017 |
haftmann <none@none> |
tuned
--HG--
extra : rebase_source : 7cd930abc368714d492a71db05fa4bb19eb14eb0
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
13683eca |
|
17-Jun-2016 |
hoelzl <none@none> |
move Conditional_Complete_Lattices to Main
--HG--
extra : rebase_source : 2cd0f07680d0081b5d3769e8a4ad49983a312a99
|
| #
9ebcfa62 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
041061bc |
|
16-Mar-2016 |
paulson <lp15@cam.ac.uk> |
Contractible sets. Also removal of obsolete theorems and refactoring
|
| #
259fcfd2 |
|
22-Feb-2016 |
paulson <lp15@cam.ac.uk> |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
6820dd05 |
|
10-Dec-2015 |
paulson <lp15@cam.ac.uk> |
not_leE -> not_le_imp_less and other tidying
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
7d3b4baf |
|
30-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
| #
66005bbd |
|
04-May-2015 |
hoelzl <none@none> |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
--HG--
extra : rebase_source : 6c7faec3b6fc45b9da856e08add46f99a0b483b7
|
| #
953196b3 |
|
27-Jan-2015 |
hoelzl <none@none> |
ereal: tuned proofs concerning continuity and suprema
--HG--
extra : rebase_source : 88d9ba24758ab75b76f4b7e10f1fc85b74642f63
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
6c0336e5 |
|
30-Jun-2014 |
hoelzl <none@none> |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141
|
| #
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
| #
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
| #
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
| #
dddd44d5 |
|
05-Nov-2013 |
hoelzl <none@none> |
int and nat are conditionally_complete_lattices
--HG--
extra : rebase_source : 4295ba08a6a68dc20cc2a24971781ce06b986aac
|
| #
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
|
| #
f77e220a |
|
05-Nov-2013 |
hoelzl <none@none> |
generalize bdd_above/below_uminus to ordered_ab_group_add
|
| #
2feba095 |
|
05-Nov-2013 |
hoelzl <none@none> |
restrict Limsup and Liminf to complete lattices
|
| #
fd02713b |
|
05-Nov-2013 |
hoelzl <none@none> |
add SUP and INF for conditionally complete lattices
|
| #
19339e2f |
|
05-Nov-2013 |
hoelzl <none@none> |
use bdd_above and bdd_below for conditionally complete lattices
|
| #
d8c6c2fb |
|
05-Nov-2013 |
hoelzl <none@none> |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
| #
0ad1a5d3 |
|
27-Aug-2013 |
hoelzl <none@none> |
renamed inner_dense_linorder to dense_linorder
--HG--
extra : rebase_source : a7a9c602f6d7437d9632ccdffa7d3b6eaafc2d01
|
| #
efe08492 |
|
27-Aug-2013 |
hoelzl <none@none> |
renamed typeclass dense_linorder to unbounded_dense_linorder
--HG--
extra : rebase_source : 1aec1d46ec989f6555ab53f40d6db74ef5536fe0
|
| #
a816b494 |
|
30-May-2013 |
wenzelm <none@none> |
tuned headers;
|
| #
812b19ed |
|
25-Apr-2013 |
hoelzl <none@none> |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
| #
09075f4b |
|
24-Apr-2013 |
hoelzl <none@none> |
spell conditional_ly_-complete lattices correct
--HG--
rename : src/HOL/Conditional_Complete_Lattices.thy => src/HOL/Conditionally_Complete_Lattices.thy
extra : rebase_source : fe25f4dff8edab189f8c7a631785ba3cc5a19aa2
|