#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
a0abd9ea |
|
07-Mar-2017 |
eberlm <eberlm@in.tum.de> |
Tuned generation of elimination rules in function package
|
#
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
|
#
53421752 |
|
09-Mar-2015 |
wenzelm <none@none> |
tuned;
|
#
65a4930c |
|
08-Mar-2015 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
554701a9 |
|
08-Mar-2015 |
wenzelm <none@none> |
tuned;
|
#
eba3c7d3 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
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;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
e7984da9 |
|
27-Jan-2015 |
eberlm <none@none> |
Fixed variable naming bug in function package
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
#
22e992a8 |
|
13-Dec-2013 |
wenzelm <none@none> |
tuned -- prefer canonical argument order of fold_rev;
|
#
39ee2fb4 |
|
13-Dec-2013 |
wenzelm <none@none> |
proper simplifier context; more standard "cert";
|
#
88d337f4 |
|
13-Dec-2013 |
wenzelm <none@none> |
tuned;
|
#
e4b35d2d |
|
13-Dec-2013 |
wenzelm <none@none> |
tuned whitespace;
|
#
2ce724a4 |
|
16-Sep-2013 |
wenzelm <none@none> |
more antiquotations -- avoid unchecked string literals;
|
#
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";
|
#
59c70b84 |
|
16-Sep-2013 |
wenzelm <none@none> |
proper Isabelle symbols -- no UTF8 here;
|
#
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)
|