| Fri, 05 Apr 2024 21:21:02 +0200 |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 14:32:50 +0000 |
paulson |
Moving valuable library material from Martingales into the distribution
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 17:06:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 16:31:17 +0200 |
wenzelm |
clarified syntax and order of parameters;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 22:29:12 +0200 |
wenzelm |
clarified simproc_setup (passive);
|
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
|
| Wed, 01 Feb 2023 20:21:33 +0100 |
wenzelm |
isabelle update -u cite -l "";
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Mon, 08 Nov 2021 19:56:15 +0100 |
nipkow |
added eq_iff_swap for creating symmetric variants of thms; applied it in List.
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 21:20:15 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:14:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2020 12:10:58 +0000 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Fri, 19 Jun 2020 09:46:47 +0000 |
haftmann |
prefer single name
|
file |
diff |
annotate
|
| Thu, 04 Jun 2020 15:30:22 +0000 |
haftmann |
more simp rules
|
file |
diff |
annotate
|
| Sat, 30 May 2020 08:50:18 +0000 |
haftmann |
install simproc but deactivate by default
|
file |
diff |
annotate
|
| Sun, 24 May 2020 19:57:13 +0000 |
haftmann |
better closeup and more consistent terminology
|
file |
diff |
annotate
|
| Wed, 13 May 2020 16:35:36 +0200 |
Manuel Eberl |
new HOL simproc: eliminate_false_implies
|
file |
diff |
annotate
|
| Tue, 12 May 2020 15:11:20 +0100 |
paulson |
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Sat, 28 Mar 2020 17:27:01 +0000 |
paulson |
structured a lot of ancient, horrible proofs
|
file |
diff |
annotate
|
| Tue, 03 Mar 2020 19:26:23 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 13:30:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Oct 2019 16:26:31 +0200 |
wenzelm |
clarified sessions/directories;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 18:41:12 +0200 |
wenzelm |
setup preprocessing for HOL proofs;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 16:46:33 +0200 |
wenzelm |
early setup of proof preprocessing;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2019 18:23:32 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 20:49:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|