| #
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
| #
ba9cb2ae |
|
18-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
| #
6c492033 |
|
07-Apr-2017 |
Lars Hupel <lars.hupel@mytum.de> |
more general signature; works for all terms, not just frees
|
| #
ae364dc0 |
|
04-Sep-2015 |
wenzelm <none@none> |
trim context for persistent storage;
tuned signature;
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
7aae2956 |
|
25-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
tuned;
|
| #
99c7a9c0 |
|
08-Jul-2015 |
wenzelm <none@none> |
Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;
|
| #
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
|
| #
4d000744 |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
more standard module name;
--HG--
rename : src/HOL/Tools/Function/context_tree.ML => src/HOL/Tools/Function/function_context_tree.ML
|