| Sun, 24 Apr 2016 20:29:49 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 11:41:11 +0100 |
wenzelm |
support for structure statements in 'assume', 'presume';
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 19:28:43 +0200 |
wenzelm |
Variable.focus etc.: optional bindings provided by user;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 10:33:37 +0200 |
wenzelm |
more robust: variables need not occur in body;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 23:22:08 +0200 |
wenzelm |
improved treatment of Element.Obtains via Expression.prepare_stmt;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 19:15:31 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 23:36:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 19:38:26 +0200 |
wenzelm |
open parameters for 'consider' rule;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 16:35:27 +0200 |
wenzelm |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 15:51:19 +0200 |
wenzelm |
clarified 'obtain', using structured 'have' statement;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 15:16:59 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 14:37:50 +0200 |
wenzelm |
clarified 'consider', using structured 'have' statement;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 15:44:00 +0200 |
wenzelm |
support to parse obtain clause without type-checking yet;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 10:44:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 16:09:49 +0200 |
wenzelm |
clarified local after_qed: result is not exported yet;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 14:46:31 +0200 |
wenzelm |
support for "if prems" in local goal statements;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 22:24:33 +0200 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:07:11 +0200 |
wenzelm |
allow for_fixes for 'have', 'show' etc.;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 13:42:58 +0200 |
wenzelm |
clarified abstracted term bindings (again, see c8384ff11711);
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 22:04:15 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 21:39:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|