isabelle: File revisions

src/Pure/subgoal.ML

2012-10-13	wenzelm	2012-10-13	tuned signature;	file \| diff \| annotate
2011-04-27	wenzelm	2011-04-27	clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;	file \| diff \| annotate
2011-04-16	wenzelm	2011-04-16	modernized structure Proof_Context;	file \| diff \| annotate
2009-12-11	wenzelm	2009-12-11	Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;	file \| diff \| annotate
2009-08-05	wenzelm	2009-08-05	SUBPROOF: recovered Goal.check_finished; tuned;	file \| diff \| annotate
2009-07-30	wenzelm	2009-07-30	retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);	file \| diff \| annotate
2009-07-30	wenzelm	2009-07-30	qualified Subgoal.FOCUS;	file \| diff \| annotate
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;	file \| diff \| annotate
2009-07-26	wenzelm	2009-07-26	added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;	file \| diff \| annotate
2009-07-26	wenzelm	2009-07-26	retrofit: actually handle schematic variables -- need to export into original context;	file \| diff \| annotate
2009-07-26	wenzelm	2009-07-26	advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;	file \| diff \| annotate
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);	file \| diff \| annotate
2009-03-16	wenzelm	2009-03-16	provide Simplifier.norm_hhf(_protect) as regular simplifier operation;	file \| diff \| annotate
2009-01-21	wenzelm	2009-01-21	removed Ids;	file \| diff \| annotate
2007-04-03	wenzelm	2007-04-03	renamed Variable.import to import_thms (avoid clash with Alice keywords);	file \| diff \| annotate
2006-11-30	wenzelm	2006-11-30	qualified MetaSimplifier.norm_hhf(_protect);	file \| diff \| annotate
2006-09-18	wenzelm	2006-09-18	Thm.dest_arg;	file \| diff \| annotate
2006-08-02	wenzelm	2006-08-02	Variable.focus_subgoal;	file \| diff \| annotate
2006-07-27	wenzelm	2006-07-27	tuned interfaces; moved basic assumption operations from structure ProofContext to Assumption;	file \| diff \| annotate
2006-07-26	wenzelm	2006-07-26	focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;	file \| diff \| annotate
2006-07-26	wenzelm	2006-07-26	Tactical operations depending on local subgoal structure.	file \| diff \| annotate

isabelle

RSS Atom