| #
7aae2956 |
|
25-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
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;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
3fe8d55b |
|
12-Nov-2013 |
blanchet <none@none> |
ported part of function package to new 'Ctr_Sugar' abstraction
|
| #
d0858517 |
|
12-Nov-2013 |
blanchet <none@none> |
undid copy-paste
|
| #
744c494f |
|
27-Jun-2013 |
wenzelm <none@none> |
tuned signature;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
7601cf1a |
|
12-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
| #
f3f5fefc |
|
21-Mar-2012 |
wenzelm <none@none> |
prefer explicitly qualified exception List.Empty;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
| #
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
| #
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
| #
2037692a |
|
23-Oct-2009 |
krauss <none@none> |
pat_completeness gets its own file
|