| Mon, 02 Dec 2019 11:57:42 +0100 |
wenzelm |
clarified export of spec rules: more like locale;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 21:29:08 +0100 |
wenzelm |
formal position for spec rule (not significant for equality);
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 15:17:23 +0100 |
wenzelm |
export spec rules;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 19:43:59 +0100 |
wenzelm |
clarified errors;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 18:55:35 +0100 |
wenzelm |
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
|
file |
diff |
annotate
|
| Mon, 21 Oct 2019 16:32:10 +0200 |
wenzelm |
export constdefs according to defs.ML;
|
file |
diff |
annotate
|
| Sun, 20 Oct 2019 12:56:36 +0200 |
wenzelm |
more kinds, notably for Isabelle/MMT;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 16:25:54 +0200 |
wenzelm |
clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 21:03:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 16:10:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 14:06:14 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 21:05:35 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:41:47 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:04:11 +0200 |
wenzelm |
support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 14:14:10 +0200 |
wenzelm |
clarified proof export;
|
file |
diff |
annotate
|