2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2012-10-13 wenzelm 2012-10-13 tuned signature;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2009-12-11 wenzelm 2009-12-11 Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
2009-08-05 wenzelm 2009-08-05 SUBPROOF: recovered Goal.check_finished; tuned;
2009-07-30 wenzelm 2009-07-30 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-30 wenzelm 2009-07-30 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed; added FOCUS_PREMS, which may serve as full replacement for OldGoals.METAHYPS;
2009-07-26 wenzelm 2009-07-26 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
2009-07-26 wenzelm 2009-07-26 retrofit: actually handle schematic variables -- need to export into original context;
2009-07-26 wenzelm 2009-07-26 advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-16 wenzelm 2009-03-16 provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-11-30 wenzelm 2006-11-30 qualified MetaSimplifier.norm_hhf(_protect);
2006-09-18 wenzelm 2006-09-18 Thm.dest_arg;
2006-08-02 wenzelm 2006-08-02 Variable.focus_subgoal;
2006-07-27 wenzelm 2006-07-27 tuned interfaces; moved basic assumption operations from structure ProofContext to Assumption;
2006-07-26 wenzelm 2006-07-26 focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;
2006-07-26 wenzelm 2006-07-26 Tactical operations depending on local subgoal structure.