#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
9d926c7e |
|
18-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
308c45ff |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
952abf53 |
|
06-Sep-2015 |
wenzelm <none@none> |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
#
53f968f4 |
|
01-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
#
90c1e718 |
|
06-Mar-2015 |
wenzelm <none@none> |
proper 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;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
47e6e8c3 |
|
31-Dec-2013 |
wenzelm <none@none> |
proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
|
#
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
|
#
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
|
#
c36c4f6a |
|
16-Oct-2011 |
wenzelm <none@none> |
added Term.dummy_pattern conveniences;
|
#
48faef5e |
|
27-Apr-2011 |
wenzelm <none@none> |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
#
9d72cd6f |
|
27-Apr-2011 |
krauss <none@none> |
inlined Function_Lib.replace_frees, which is used only once
|
#
d3a207ad |
|
27-Apr-2011 |
wenzelm <none@none> |
eliminated obsolete Function_Lib.frees_in_term; simplified;
|
#
1a848c94 |
|
13-Dec-2010 |
krauss <none@none> |
eliminated dest_all_all_ctx
|
#
a83bf3cb |
|
13-Dec-2010 |
krauss <none@none> |
private term variant of Variable.focus
|
#
f1a21585 |
|
12-Dec-2010 |
krauss <none@none> |
added signature; more honest header
|
#
637fe2f1 |
|
26-Nov-2010 |
wenzelm <none@none> |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
#
0dc105bc |
|
22-Oct-2010 |
krauss <none@none> |
some cleanup in Function_Lib
|
#
a00eb206 |
|
27-Sep-2010 |
krauss <none@none> |
consolidated tupled_lambda; moved to structure HOLogic
|
#
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
#
42aff2ea |
|
09-Jun-2010 |
haftmann <none@none> |
tuned quotes, antiquotations and whitespace
|
#
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
#
5e512ec7 |
|
27-Feb-2010 |
wenzelm <none@none> |
clarified @{const_name} vs. @{const_abbrev};
|
#
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
#
4678ef3f |
|
23-Nov-2009 |
krauss <none@none> |
eliminated dead code and some unused bindings, reported by polyml
|
#
1332646c |
|
11-Nov-2009 |
haftmann <none@none> |
tuned
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|