#
fad9031b |
|
19-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
5afa6b71 |
|
11-Sep-2017 |
wenzelm <none@none> |
clarified signature: proper result;
|
#
2f76843d |
|
11-Sep-2017 |
wenzelm <none@none> |
clarified signature: proper result;
|
#
46bb214d |
|
11-Jun-2016 |
wenzelm <none@none> |
clarified syntax;
|
#
86d79029 |
|
30-May-2016 |
wenzelm <none@none> |
allow 'for' fixes for multi_specs;
|
#
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
#
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
|
#
238a1740 |
|
18-Apr-2016 |
wenzelm <none@none> |
avoid clash with function called "x";
|
#
308c45ff |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
ef845594 |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified signature;
|
#
020aed70 |
|
16-Apr-2016 |
wenzelm <none@none> |
clarified reported positions;
|
#
e34d2624 |
|
16-Apr-2016 |
wenzelm <none@none> |
operate on proper binding; tuned;
|
#
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
57790ccb |
|
14-Dec-2015 |
wenzelm <none@none> |
tuned signature;
|
#
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
|
#
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
#
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';
|
#
546c1ec1 |
|
04-Sep-2015 |
wenzelm <none@none> |
trim context for persistent storage;
|
#
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
#
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;
|
#
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local 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;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems; modernized module name and setup;
|
#
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;
|
#
eb5ad205 |
|
05-Dec-2013 |
Andreas Lochbihler <none@none> |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
#
0e647e52 |
|
12-Nov-2013 |
blanchet <none@none> |
ported 'partial_function' to 'Ctr_Sugar' abstraction
|
#
3cde49ef |
|
24-Jul-2013 |
krauss <none@none> |
derive specialized version of full fixpoint induction (with admissibility)
|
#
0261341b |
|
24-Jul-2013 |
krauss <none@none> |
export mono_thm
|
#
aea7279c |
|
02-Jul-2013 |
krauss <none@none> |
more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering
|
#
2680e2ce |
|
20-May-2013 |
wenzelm <none@none> |
more precise treatment of theory vs. Proof.context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
c183e800 |
|
21-Mar-2013 |
krauss <none@none> |
allow induction predicates with arbitrary arity (not just binary)
|
#
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
#
de9fb383 |
|
15-Mar-2012 |
wenzelm <none@none> |
prefer formally checked @{keyword} parser;
|
#
476fb08c |
|
08-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
50fe8111 |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned Named_Thms: proper binding;
|
#
eec33c84 |
|
19-Sep-2011 |
krauss <none@none> |
match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test
|
#
ac71d3a2 |
|
31-May-2011 |
krauss <none@none> |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
#
e73bb49a |
|
23-May-2011 |
krauss <none@none> |
also manage induction rule; tuned data slot
|
#
bc71ee3c |
|
23-May-2011 |
krauss <none@none> |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
#
48faef5e |
|
27-Apr-2011 |
wenzelm <none@none> |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
#
c067ae81 |
|
18-Apr-2011 |
wenzelm <none@none> |
standardized aliases of operations on tsig;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
6701cdc1 |
|
24-Mar-2011 |
wenzelm <none@none> |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
#
ef2d6500 |
|
08-Jan-2011 |
wenzelm <none@none> |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
#
1a848c94 |
|
13-Dec-2010 |
krauss <none@none> |
eliminated dest_all_all_ctx
|
#
72600e52 |
|
26-Oct-2010 |
haftmann <none@none> |
partial_function is a declaration command
|
#
44b17632 |
|
26-Oct-2010 |
krauss <none@none> |
fixed confusion introduced in 008dc2d2c395
|
#
b8ddfe71 |
|
25-Oct-2010 |
krauss <none@none> |
added Spec_Rule declaration to partial_function
|
#
17911f6f |
|
25-Oct-2010 |
krauss <none@none> |
declare recursive equation as ".simps", in accordance with other packages
|
#
ae451101 |
|
23-Oct-2010 |
krauss <none@none> |
first version of partial_function package
|