| Sun, 17 Apr 2016 12:40:48 +0200 |
wenzelm |
clarified reported positions;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 12:26:22 +0200 |
wenzelm |
operate on proper binding;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2015 11:20:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 21:55:13 +0200 |
wenzelm |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 14:00:13 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
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, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|