| Sat, 02 Dec 2023 15:42:50 +0100 |
wenzelm |
pro-forma support for optional zproof: no proper content yet;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 18:45:41 +0200 |
wenzelm |
clarified signature: avoid association with potentially dangerous Exn.capture;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2023 20:15:31 +0200 |
wenzelm |
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:42:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2023 21:00:24 +0200 |
wenzelm |
tuned: concise combinators instead of bulky case-expressions;
|
file |
diff |
annotate
|
| Thu, 08 Sep 2022 13:16:46 +0200 |
wenzelm |
removed odd TODO item (see 3391a493f39a);
|
file |
diff |
annotate
|
| Thu, 08 Sep 2022 13:13:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2022 21:15:45 +0200 |
wenzelm |
print goal instantiation for global qed (and variations);
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 21:13:29 +0200 |
wenzelm |
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 19:23:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 17:53:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 13:32:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 11:36:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2022 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 13 Oct 2021 13:21:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 15:09:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 22:46:01 +0200 |
wenzelm |
support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 21:35:21 +0200 |
wenzelm |
proper export of result_text for 'have';
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:53:53 +0200 |
wenzelm |
support soft types for 'assume';
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:10:15 +0200 |
wenzelm |
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 17:06:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 16:26:57 +0200 |
wenzelm |
clarified signature -- removed unused option (see acb0807ddb56);
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 21:49:31 +0200 |
wenzelm |
discontinued old-style goal cases;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 19:48:15 +0200 |
wenzelm |
clarified reset_notepad;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 13:53:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|