src/Pure/subgoal.ML
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.