| Wed, 18 Mar 2020 20:04:50 +0100 | wenzelm | slightly more explicit error, without going into the graph of proof futures; | file | diff | annotate |
| Thu, 12 Mar 2020 20:58:18 +0100 | wenzelm | proper transfer for Thm.derivation_name; | file | diff | annotate |
| Mon, 24 Feb 2020 20:57:29 +0100 | wenzelm | more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1; | 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 |
| Thu, 31 Oct 2019 21:21:09 +0100 | wenzelm | clarified signature; | file | diff | annotate |
| Thu, 31 Oct 2019 14:29:29 +0100 | wenzelm | clarified signature; | file | diff | annotate |
| Thu, 17 Oct 2019 20:56:18 +0200 | wenzelm | proof boxes based on proof digest (not proof term): thus it works with prune_proofs; | file | diff | annotate |
| Thu, 17 Oct 2019 20:28:31 +0200 | wenzelm | clarified files; | file | diff | annotate | base |