#
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
|
#
a975a1d1 |
|
06-Oct-2015 |
wenzelm <none@none> |
avoid hardwired frees; tuned;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
cff2e75b |
|
08-Apr-2015 |
wenzelm <none@none> |
proper context for Object_Logic operations;
|
#
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
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
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;
|
#
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
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;
|
#
744c494f |
|
27-Jun-2013 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
7601cf1a |
|
12-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
#
15a38bfc |
|
14-Feb-2012 |
wenzelm <none@none> |
comment;
|
#
ab54c3b1 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
#
48faef5e |
|
27-Apr-2011 |
wenzelm <none@none> |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
5885238e |
|
29-Dec-2010 |
krauss <none@none> |
more robust decomposition of simultaneous goals
|
#
3272990d |
|
17-Dec-2010 |
wenzelm <none@none> |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning; --HG-- rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML
|
#
a524ad75 |
|
17-Dec-2010 |
wenzelm <none@none> |
refer to regular structure Simplifier;
|
#
1a848c94 |
|
13-Dec-2010 |
krauss <none@none> |
eliminated dest_all_all_ctx
|
#
a00eb206 |
|
27-Sep-2010 |
krauss <none@none> |
consolidated tupled_lambda; moved to structure HOLogic
|
#
b6d43d5c |
|
01-Jul-2010 |
haftmann <none@none> |
qualified constants Set.member and Set.Collect
|
#
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
#
c3452482 |
|
06-Mar-2010 |
wenzelm <none@none> |
modernized structure Object_Logic;
|
#
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
|
#
105f07d1 |
|
15-Nov-2009 |
wenzelm <none@none> |
tuned;
|
#
9a87f2e3 |
|
06-Nov-2009 |
krauss <none@none> |
renamed method induct_scheme to induction_schema
|