| #
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
| #
457def15 |
|
08-Apr-2015 |
wenzelm <none@none> |
more standard access to specific subgoal;
|
| #
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
|
| #
de8e2f0e |
|
19-Dec-2014 |
wenzelm <none@none> |
just one data slot per program unit;
tuned signature;
|
| #
429ef7fe |
|
23-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
| #
de2f0b64 |
|
08-Nov-2010 |
krauss <none@none> |
removed type-inference-like behaviour from relation_tac completely; tuned
|
| #
8b92d5ce |
|
22-Oct-2010 |
krauss <none@none> |
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
|
| #
7a8a04cd |
|
04-May-2010 |
krauss <none@none> |
avoid exception Empty on malformed goal
|
| #
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
| #
f6facf8e |
|
23-Oct-2009 |
krauss <none@none> |
renamed auto_term.ML -> relation.ML
|