#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
45f9fa0b |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
1f4a8ca3 |
|
12-Nov-2014 |
wenzelm <none@none> |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
#
6a3623e0 |
|
08-Mar-2014 |
wenzelm <none@none> |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
|
#
a00b1b4a |
|
30-Sep-2013 |
wenzelm <none@none> |
tuned signature;
|
#
2eaa7e48 |
|
30-Sep-2013 |
wenzelm <none@none> |
eliminated clone of Inductive.mk_cases_tac;
|
#
e380abce |
|
30-Sep-2013 |
wenzelm <none@none> |
tuned signature;
|
#
ea011a03 |
|
30-Sep-2013 |
wenzelm <none@none> |
tuned whitespace;
|
#
7cf78efd |
|
30-Sep-2013 |
wenzelm <none@none> |
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
|
#
d3a980ee |
|
16-Sep-2013 |
wenzelm <none@none> |
tuned signature;
|
#
982d66b3 |
|
16-Sep-2013 |
wenzelm <none@none> |
more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);
|
#
801d1ee3 |
|
16-Sep-2013 |
wenzelm <none@none> |
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions; some notes about missing ML interface;
|
#
38d6eb36 |
|
16-Sep-2013 |
wenzelm <none@none> |
tuned white space; avoid "object-oriented English";
|
#
80fb7840 |
|
08-Sep-2013 |
krauss <none@none> |
dropped unnecessary 'open'
|
#
6b6082d7 |
|
08-Sep-2013 |
krauss <none@none> |
tuned headers
|
#
68e03336 |
|
08-Sep-2013 |
Manuel Eberl <none@none> |
generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)
|