| Thu, 22 Dec 2022 18:32:42 +0000 |
paulson |
A few new Sup/Inf lemmas
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Mon, 30 May 2022 12:46:11 +0100 |
paulson |
Five slightly useful lemmas
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 14:43:25 +0100 |
paulson |
A few new lemmas and simplifications
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Mon, 22 Feb 2021 07:49:51 +0000 |
haftmann |
dedicated locale for preorder and abstract bdd operation
|
file |
diff |
annotate
|
| Tue, 12 May 2020 16:53:02 +0100 |
paulson |
Fixes for Sup{} = (0::nat)
|
file |
diff |
annotate
|
| Tue, 12 May 2020 15:11:20 +0100 |
paulson |
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 12:09:33 +0000 |
haftmann |
removed some vain declarations
|
file |
diff |
annotate
|
| Tue, 12 Nov 2019 12:33:05 +0000 |
paulson |
New library material from the AFP entry ZFC_in_HOL
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 17:54:49 +0100 |
immler |
moved some material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:19 +0000 |
haftmann |
clarified status of legacy input abbreviations
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 01:04:23 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 22 Jan 2018 15:25:46 +0100 |
nipkow |
removed duplicate
|
file |
diff |
annotate
|
| Fri, 19 Jan 2018 15:42:53 +0100 |
nipkow |
moved from AFP/Gromov
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 09:27:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 09:44:16 +0200 |
hoelzl |
move Conditional_Complete_Lattices to Main
|
file |
diff |
annotate
|
| Fri, 27 May 2016 23:35:13 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 13:56:16 +0100 |
paulson |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
file |
diff |
annotate
|
| Mon, 04 May 2015 17:35:31 +0200 |
hoelzl |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file |
diff |
annotate
|
| Tue, 27 Jan 2015 16:12:40 +0100 |
hoelzl |
ereal: tuned proofs concerning continuity and suprema
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 21:23:42 +0100 |
hoelzl |
int and nat are conditionally_complete_lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:00 +0100 |
hoelzl |
generalize bdd_above/below_uminus to ordered_ab_group_add
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:00 +0100 |
hoelzl |
restrict Limsup and Liminf to complete lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:59 +0100 |
hoelzl |
add SUP and INF for conditionally complete lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:57 +0100 |
hoelzl |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:06:27 +0200 |
hoelzl |
renamed inner_dense_linorder to dense_linorder
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 14:37:56 +0200 |
hoelzl |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file |
diff |
annotate
|
| Thu, 30 May 2013 23:29:33 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 11:59:21 +0200 |
hoelzl |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:28:30 +0200 |
hoelzl |
spell conditional_ly_-complete lattices correct
|
file |
diff |
annotate
| base
|