| Mon, 23 Oct 2023 16:19:19 +0100 | paulson | Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal. | file | diff | annotate |
| Fri, 15 Oct 2021 19:25:31 +0200 | wenzelm | discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; | file | diff | annotate |
| Wed, 01 May 2019 10:40:40 +0000 | haftmann | more correct simulation of eigen context for generated Isar statements | file | diff | annotate |
| Sat, 30 Mar 2019 15:37:27 +0100 | haftmann | experimental commands for proof sketching and exploration | file | diff | annotate |