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
|