| Fri, 02 Feb 2024 11:25:11 +0000 |
paulson |
A small number of new lemmas
|
file |
diff |
annotate
|
| Thu, 30 Nov 2023 16:56:44 +0100 |
nipkow |
added and removed [simp]s
|
file |
diff |
annotate
|
| Thu, 06 Jul 2023 16:59:12 +0100 |
paulson |
The sym_diff operator (symmetric difference)
|
file |
diff |
annotate
|
| Fri, 30 Jun 2023 08:17:27 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| 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, 02 May 2023 15:17:39 +0100 |
paulson |
More new theorems, and a necessary correction
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Tue, 11 Oct 2022 10:45:42 +0200 |
nipkow |
moved theorem from Fun to Set
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 13:21:27 +0200 |
desharna |
moved mono and strict_mono to Fun and redefined them as abbreviations
|
file |
diff |
annotate
|
| Tue, 26 Oct 2021 11:15:40 +0100 |
paulson |
Added / moved some simple set-theoretic lemmas
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Tue, 11 May 2021 15:50:19 +0100 |
paulson |
Just one lemma
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
dissolve theory with duplicated name from afp
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 13:08:13 +0000 |
paulson |
trival
|
file |
diff |
annotate
|
| Tue, 10 Nov 2020 23:21:04 +0000 |
paulson |
cleanup
|
file |
diff |
annotate
|
| Sun, 24 May 2020 19:57:13 +0000 |
haftmann |
better closeup and more consistent terminology
|
file |
diff |
annotate
|
| Wed, 20 May 2020 15:00:25 +0100 |
paulson |
A few new theorems, plus some tidying up
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 17:08:51 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 17:01:36 +0000 |
paulson |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
file |
diff |
annotate
|
| Thu, 21 Mar 2019 14:18:22 +0000 |
paulson |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
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
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| Sun, 11 Nov 2018 13:05:15 +0100 |
nipkow |
more [simp]
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 08:19:06 +0200 |
nipkow |
added lemma
|
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
|
| Wed, 22 Aug 2018 12:32:57 +0000 |
haftmann |
new simp rule
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 10:13:42 +0100 |
nipkow |
line break before op was intentional
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 18:18:34 +0100 |
nipkow |
tuned notation
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:21:49 +0100 |
nipkow |
Manual updates towards conversion of "op" syntax
|
file |
diff |
annotate
|
| Sun, 31 Dec 2017 21:42:20 +0000 |
paulson |
Restored correct spacing for set comprehensions
|
file |
diff |
annotate
|
| Fri, 22 Dec 2017 21:00:07 +0000 |
paulson |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
canonical introduction and destruction rules for pairwise
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 18:52:34 +0200 |
hoelzl |
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 15:44:47 +0100 |
paulson |
More mainly topological results
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 14:14:49 +0100 |
paulson |
simple new lemmas, mostly about sets
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 23:39:49 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 22:23:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Sun, 19 Jun 2016 22:51:42 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 15:34:21 +0100 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| Fri, 27 May 2016 23:35:13 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 15:33:24 +0100 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Mon, 09 May 2016 16:02:23 +0100 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:30:32 +0100 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 16:52:56 +0100 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|