| Fri, 24 Sep 2021 22:23:26 +0200 |
wenzelm |
tuned proofs --- avoid 'guess';
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 10:27:47 +0100 |
nipkow |
more canonical and less specialized syntax
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 22:57:16 +0000 |
Angeliki KoutsoukouArgyraki |
minor tagging updates in 13 theories
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 11:59:19 +0000 |
Angeliki KoutsoukouArgyraki |
updated tagging first 5
|
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
|
| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
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
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
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
|
| Tue, 20 Feb 2018 22:25:23 +0100 |
wenzelm |
tuned proofs -- prefer explicit names for facts from 'interpret';
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
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
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|