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