| Tue, 28 Feb 2023 16:46:56 +0000 |
paulson |
Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 17:36:26 +0200 |
traytel |
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
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
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:12:37 +0200 |
nipkow |
Keep filter input syntax
|
file |
diff |
annotate
|
| Tue, 22 May 2018 11:08:37 +0200 |
nipkow |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
|
file |
diff |
annotate
|
| Fri, 13 Apr 2018 15:58:27 +0100 |
paulson |
Probability builds with new definitions
|
file |
diff |
annotate
|
| Sun, 11 Feb 2018 18:09:17 +0100 |
Lars Hupel |
use preferred resolver according to DOI Handbook §3.8
|
file |
diff |
annotate
|
| Tue, 23 Jan 2018 12:28:46 +0100 |
Lars Hupel |
drop redundant cong rules
|
file |
diff |
annotate
|
| Mon, 22 Jan 2018 15:50:29 +0100 |
Lars Hupel |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
| Thu, 31 Aug 2017 17:48:20 +0200 |
eberlm |
Connecting PMFs to infinite sums
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 14:26:03 +0100 |
paulson |
A few renamings and several tidied-up proofs
|
file |
diff |
annotate
|
| Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 08:57:21 +0200 |
eberlm |
moved material from AFP to distribution
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 08:43:30 +0100 |
haftmann |
proper logical constants
|
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
|
| Fri, 30 Sep 2016 15:35:46 +0200 |
hoelzl |
Probability: fix proof
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 13:56:51 +0200 |
hoelzl |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|