#
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
6c492033 |
|
07-Apr-2017 |
Lars Hupel <lars.hupel@mytum.de> |
more general signature; works for all terms, not just frees
|
#
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
#
9d926c7e |
|
18-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
308c45ff |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
c7340223 |
|
17-Apr-2016 |
wenzelm <none@none> |
prefer binding over base name;
|
#
bd54f2fd |
|
17-Apr-2016 |
wenzelm <none@none> |
prefer precise names for internal construction;
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
a975a1d1 |
|
06-Oct-2015 |
wenzelm <none@none> |
avoid hardwired frees; tuned;
|
#
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';
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
a804eb03 |
|
05-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
#
093cea8d |
|
31-Mar-2015 |
wenzelm <none@none> |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
#
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
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
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
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
|
#
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
#
da328fb3 |
|
07-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
e99c6e6b |
|
12-Feb-2014 |
blanchet <none@none> |
got rid of dynamic scoping the easy way
|
#
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain --HG-- rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|
#
68e03336 |
|
08-Sep-2013 |
Manuel Eberl <none@none> |
generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)
|
#
744c494f |
|
27-Jun-2013 |
wenzelm <none@none> |
tuned signature;
|
#
47ff4e33 |
|
26-Jun-2013 |
wenzelm <none@none> |
tuned signature;
|
#
6e401e29 |
|
16-Jun-2013 |
krauss <none@none> |
export dom predicate in the info record
|
#
1b1fb1e5 |
|
29-May-2013 |
wenzelm <none@none> |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
6aed1976 |
|
05-Sep-2012 |
wenzelm <none@none> |
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
|
#
ab54c3b1 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
d3a207ad |
|
27-Apr-2011 |
wenzelm <none@none> |
eliminated obsolete Function_Lib.frees_in_term; simplified;
|
#
342b80ce |
|
16-Apr-2011 |
wenzelm <none@none> |
observe firm naming convention ctxt: Proof.context;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
8caff1de |
|
25-Feb-2011 |
krauss <none@none> |
removed support for tail-recursion from function package (now implemented by partial_function)
|
#
08819991 |
|
29-Dec-2010 |
krauss <none@none> |
function (default) is legacy feature
|
#
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
#
96fc9813 |
|
12-Sep-2010 |
wenzelm <none@none> |
eliminated aliases of Type.constraint;
|
#
336229db |
|
31-Aug-2010 |
krauss <none@none> |
more permissive: simplification solves the goal when rhs = undefined
|
#
33076e76 |
|
19-Aug-2010 |
haftmann <none@none> |
tuned quotes
|
#
bbda5041 |
|
19-Aug-2010 |
haftmann <none@none> |
use antiquotations for remaining unqualified constants in HOL
|
#
b7e81c3e |
|
27-May-2010 |
wenzelm <none@none> |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
#
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
#
4d41603e |
|
15-May-2010 |
wenzelm <none@none> |
incorporated further conversions and conversionals, after some minor tuning;
|
#
fc5d3dfa |
|
21-Apr-2010 |
krauss <none@none> |
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
|
#
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
#
ab8ebe11 |
|
11-Dec-2009 |
haftmann <none@none> |
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
|
#
4678ef3f |
|
23-Nov-2009 |
krauss <none@none> |
eliminated dead code and some unused bindings, reported by polyml
|
#
8d32b36e |
|
19-Nov-2009 |
wenzelm <none@none> |
adapted Local_Theory.define -- eliminated odd thm kind;
|
#
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
#
29a60963 |
|
13-Nov-2009 |
wenzelm <none@none> |
inductive: eliminated obsolete kind;
|
#
d4527641 |
|
12-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
#
e4322cd7 |
|
29-Oct-2009 |
krauss <none@none> |
less verbose inductive invocation
|
#
0f5c853c |
|
29-Oct-2009 |
krauss <none@none> |
tuned
|
#
1ee0626a |
|
29-Oct-2009 |
krauss <none@none> |
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
|
#
ca381023 |
|
28-Oct-2009 |
wenzelm <none@none> |
conceal internal bindings;
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|