#
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
|