| Thu, 18 Apr 2024 17:53:14 +0200 |
Simon Wimmer |
sketch & explore: recover from duplicate fixed variables in Isar proofs
|
file |
diff |
annotate
|
| Sat, 13 Apr 2024 10:22:14 +0200 |
Simon Wimmer |
Add subgoals variant of 'sketch' command
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 21:46:31 +0100 |
Simon Wimmer |
sketch & explore: TODO comments are addressed in parent commits
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 21:11:23 +0100 |
Simon Wimmer |
sketch & explore: reduce unnecessary type constraints
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 21:20:36 +0100 |
Simon Wimmer |
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 21:31:18 +0100 |
Simon Wimmer |
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
|
file |
diff |
annotate
|
| Sat, 09 Mar 2024 11:35:32 +0100 |
wenzelm |
eliminate odd aliases (see also 2746dfc9ceae);
|
file |
diff |
annotate
|
| Tue, 27 Feb 2024 13:46:42 +0100 |
Simon Wimmer |
optional cartouche syntax and proper name printing in atp Isar output
|
file |
diff |
annotate
|
| 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
|