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