| Wed, 02 Oct 2024 10:35:44 +0200 |
wenzelm |
more inner syntax markup: HOL-Analysis;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 21:10:01 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2024 22:47:44 +0100 |
paulson |
New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero
|
file |
diff |
annotate
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 15:33:45 +0000 |
paulson |
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
|
file |
diff |
annotate
|
| Thu, 03 Aug 2023 19:10:36 +0200 |
paulson |
More cosmetic changes
|
file |
diff |
annotate
|
| Fri, 24 Sep 2021 22:23:26 +0200 |
wenzelm |
tuned proofs --- avoid '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
|
| Wed, 07 Apr 2021 12:28:19 +0000 |
haftmann |
simplified definition
|
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
|
| Thu, 14 May 2020 13:44:44 +0200 |
Manuel Eberl |
Tuned some proofs in HOL-Analysis
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Wed, 15 May 2019 14:43:32 +0100 |
paulson |
a few general lemmas
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 14:59:40 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 22:57:16 +0000 |
Angeliki KoutsoukouArgyraki |
minor tagging updates in 13 theories
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 11:59:19 +0000 |
Angeliki KoutsoukouArgyraki |
updated tagging first 5
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2018 10:34:56 +0000 |
haftmann |
prefer naming convention from datatype package for strong congruence rules
|
file |
diff |
annotate
|
| Wed, 17 Oct 2018 14:19:07 +0100 |
paulson |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
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
|
| Tue, 28 Aug 2018 13:28:39 +0100 |
Angeliki KoutsoukouArgyraki |
tagged 21 theories in the Analysis library for the manual
|
file |
diff |
annotate
|