| Tue, 08 Oct 2024 12:10:35 +0200 |
wenzelm |
more inner-syntax markup;
|
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
|
| Thu, 11 Apr 2024 18:46:49 +0000 |
haftmann |
prefer canonical theorem name for fact collection declarations
|
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
|
| 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, 16 Jul 2021 14:43:25 +0100 |
paulson |
A few new lemmas and simplifications
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Fri, 10 Apr 2020 22:50:59 +0100 |
paulson |
more removal of applys
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 21:58:42 +0000 |
haftmann |
more rules for natural deduction from inequalities
|
file |
diff |
annotate
|
| Sat, 09 Nov 2019 10:38:51 +0000 |
haftmann |
new lemma
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Thu, 08 Aug 2019 12:11:40 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
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
|