isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/Pure/subgoal.ML

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

less more (0) tip

isabelle

RSS Atom