| 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
|