2009-12-11 ago Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
2009-08-05 ago SUBPROOF: recovered Goal.check_finished;
2009-07-30 ago retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
2009-07-30 ago qualified Subgoal.FOCUS;
2009-07-30 ago focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
2009-07-26 ago added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
2009-07-26 ago retrofit: actually handle schematic variables -- need to export into original context;
2009-07-26 ago advanced retrofit, which allows new subgoals and variables;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-16 ago provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-01-21 ago removed Ids;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-11-30 ago qualified MetaSimplifier.norm_hhf(_protect);
2006-09-18 ago Thm.dest_arg;
2006-08-02 ago Variable.focus_subgoal;
2006-07-27 ago tuned interfaces;
2006-07-26 ago focus: result record includes (fixed) schematic variables;
2006-07-26 ago Tactical operations depending on local subgoal structure.