| 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
|