| Tue, 23 May 2023 21:43:36 +0200 |
wenzelm |
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 11:59:02 +0000 |
haftmann |
proper section headings
|
file |
diff |
annotate
|
| Sun, 11 Sep 2022 13:27:39 +0100 |
paulson |
tidied a few ugly proofs
|
file |
diff |
annotate
|
| Sat, 30 Oct 2021 17:10:10 +0200 |
wenzelm |
tuned proofs -- avoid z3, which is unavailable on arm64-linux;
|
file |
diff |
annotate
|
| Wed, 06 Oct 2021 14:19:46 +0200 |
eberlm |
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 13:52:09 +0200 |
wenzelm |
tuned proofs --- eliminated 'guess';
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Wed, 23 Jun 2021 17:43:31 +0000 |
haftmann |
more default simp rules
|
file |
diff |
annotate
|
| Fri, 19 Feb 2021 13:42:12 +0100 |
Manuel Eberl |
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
|
file |
diff |
annotate
|
| Tue, 01 Sep 2020 22:01:27 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Tue, 12 May 2020 16:53:02 +0100 |
paulson |
Fixes for Sup{} = (0::nat)
|
file |
diff |
annotate
|
| Fri, 19 Jul 2019 12:57:14 +0100 |
paulson |
More results about measure and integration theory
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 15:40:15 +0100 |
paulson |
More analysis / measure theory material
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 14:08:28 +0100 |
paulson |
more new material about analysis
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 15 May 2019 14:43:32 +0100 |
paulson |
a few general lemmas
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 07:00:21 +0000 |
haftmann |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 09:43:48 +0200 |
nipkow |
(re)moved lemmas
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:54:55 +0000 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 09:28:14 +0000 |
paulson |
fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
|
file |
diff |
annotate
|
| Fri, 19 Jan 2018 08:28:08 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 17 Jan 2018 12:27:06 +0100 |
nipkow |
more lemmas by Gouezele
|
file |
diff |
annotate
|
| Wed, 17 Jan 2018 09:55:03 +0100 |
nipkow |
move lemmas by Gouezel to distribution
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 09:18:54 +0000 |
haftmann |
restored naming of lemmas after corresponding constants
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Wed, 03 May 2017 14:39:04 +0100 |
paulson |
two new theorems
|
file |
diff |
annotate
|
| Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| Fri, 28 Oct 2016 19:54:41 +0200 |
kuncar |
a more general relator domain rule for the function type
|
file |
diff |
annotate
|
| Thu, 20 Oct 2016 18:41:59 +0200 |
hoelzl |
HOL-Probability: move stopping time from AFP/Markov_Models
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 12:01:54 +0200 |
hoelzl |
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 16:08:38 +0200 |
hoelzl |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:16:35 +0200 |
wenzelm |
clarified lfp/gfp statements and proofs;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2016 10:26:04 +0200 |
hoelzl |
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 08:02:37 +0200 |
wenzelm |
tuned proofs -- avoid improper use of "this";
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 17:47:47 +0200 |
hoelzl |
move ennreal and ereal theorems from MFMC_Countable
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:44:31 +0200 |
wenzelm |
some uses of 'obtain' with structure statement;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:48:11 +0200 |
hoelzl |
Probability: move emeasure and nn_integral from ereal to ennreal
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 14:48:14 +0100 |
hoelzl |
more stuff for extended nonnegative real numbers
|
file |
diff |
annotate
|
| Tue, 15 Mar 2016 14:08:25 +0000 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
| Tue, 09 Feb 2016 09:21:10 +0100 |
hoelzl |
add extended nonnegative real numbers
|
file |
diff |
annotate
|