| Thu, 03 Jul 2025 13:53:14 +0200 |
nipkow |
removed duplicate lemma; added the notion of the kernel of a function
|
file |
diff |
annotate
|
| Thu, 03 Apr 2025 21:08:36 +0100 |
paulson |
Lemmas from Manuel Eberl's Q_Analogues
|
file |
diff |
annotate
|
| Mon, 31 Mar 2025 22:46:11 +0100 |
paulson |
Some generalisations (mostly at the level of type classes) by Alexander Pach
|
file |
diff |
annotate
|
| Tue, 25 Feb 2025 15:54:41 +0100 |
desharna |
added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)
|
file |
diff |
annotate
|
| Fri, 21 Feb 2025 18:46:59 +0100 |
nipkow |
weakened type class (thanks to Alexander Pach)
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 14:59:57 +0100 |
wenzelm |
more syntax bundles, e.g. to explore terms without notation;
|
file |
diff |
annotate
|
| Sun, 08 Dec 2024 15:12:20 +0100 |
wenzelm |
tuned: prefer explicit names of inferred types;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 12:10:35 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Tue, 01 Oct 2024 20:39:16 +0200 |
wenzelm |
drop somewhat pointless 'syntax_consts' declarations;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2024 13:00:42 +0200 |
wenzelm |
less markup: prefer "notatation" over "entity";
|
file |
diff |
annotate
|
| 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
|
| Wed, 07 Aug 2024 16:28:32 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Tue, 13 Feb 2024 17:18:50 +0000 |
paulson |
A few lemmas brought in from AFP entries
|
file |
diff |
annotate
|
| Tue, 06 Feb 2024 15:29:10 +0000 |
paulson |
Correct the definition of a convex function, and updated the proofs
|
file |
diff |
annotate
|
| Thu, 06 Jul 2023 16:59:12 +0100 |
paulson |
The sym_diff operator (symmetric difference)
|
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 12:51:05 +0100 |
paulson |
A few new theorems
|
file |
diff |
annotate
|
| Mon, 30 Jan 2023 15:24:17 +0000 |
paulson |
Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 17:59:44 +0000 |
paulson |
First round of moving material from the number theory development
|
file |
diff |
annotate
|
| Thu, 13 Oct 2022 14:27:15 +0200 |
desharna |
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset
|
file |
diff |
annotate
|
| Wed, 12 Oct 2022 08:21:07 +0200 |
nipkow |
one more lemma
|
file |
diff |
annotate
|
| Tue, 11 Oct 2022 14:22:11 +0200 |
nipkow |
added and reorganized lemmas (some suggested by Jeremy Sylvestre)
|
file |
diff |
annotate
|
| Tue, 11 Oct 2022 12:13:47 +0200 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Tue, 11 Oct 2022 10:45:42 +0200 |
nipkow |
moved theorem from Fun to Set
|
file |
diff |
annotate
|
| Sat, 08 Oct 2022 18:35:53 +0200 |
nipkow |
generalized type classes as suggested by Jeremy Sylvestre
|
file |
diff |
annotate
|
| Fri, 02 Sep 2022 13:41:55 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 13:34:41 +0200 |
desharna |
moved antimono to Fun and redefined it as an abbreviation
|
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
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|