| Tue, 04 Jun 2019 15:11:29 +0200 |
wenzelm |
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 13:39:34 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 18:18:38 +0100 |
wenzelm |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 14:17:27 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:45:17 +0200 |
wenzelm |
eliminated clone of Inductive.mk_cases_tac;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:35:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:29:09 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:20:44 +0200 |
wenzelm |
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 19:27:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 17:18:56 +0200 |
wenzelm |
more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 17:13:38 +0200 |
wenzelm |
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 17:04:28 +0200 |
wenzelm |
tuned white space;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 00:59:45 +0200 |
krauss |
dropped unnecessary 'open'
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 00:53:50 +0200 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 22:32:47 +0200 |
Manuel Eberl |
generate elim rules for elimination of function equalities;
|
file |
diff |
annotate
|