| Mon, 23 Sep 2024 21:09:23 +0200 |
wenzelm |
more inner syntax markup: HOL;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:02:19 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2022 19:29:22 +0200 |
desharna |
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
tuned theory structure
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
lemma diffusion
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 17:12:26 +0100 |
paulson |
Tidied up more ancient, horrible proofs. Liberalised frac_le
|
file |
diff |
annotate
|
| Sat, 14 Mar 2020 15:58:51 +0000 |
paulson |
tidied up a few little proofs
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 21:53:45 +0100 |
paulson |
moved subset_image_inj into Hilbert_Choice
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
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
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2018 08:16:42 +0000 |
haftmann |
tuned proof text
|
file |
diff |
annotate
|
| Wed, 19 Dec 2018 08:16:41 +0000 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:19 +0000 |
haftmann |
clarified status of legacy input abbreviations
|
file |
diff |
annotate
|
| Tue, 11 Sep 2018 16:21:54 +0100 |
paulson |
A few new results, elimination of duplicates and more use of "pairwise"
|
file |
diff |
annotate
|
| Fri, 24 Aug 2018 20:22:14 +0000 |
haftmann |
some modernization of notation
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 01:04:23 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Mon, 26 Mar 2018 16:14:16 +0200 |
Manuel Eberl |
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 20:52:53 +0100 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
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
|
| Sun, 28 May 2017 15:46:26 +0200 |
nipkow |
removed GreatestM
|
file |
diff |
annotate
|