--- a/src/Pure/Isar/isar_syn.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 01 21:29:57 2015 +0200
@@ -679,6 +679,32 @@
Toplevel.skip_proof (fn i => i + 1))));
+(* subgoal focus *)
+
+local
+
+val opt_fact_binding =
+ Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+ Attrib.empty_binding;
+
+val params =
+ Parse.binding -- Parse.mixfix' >> single || Scan.repeat1 Parse.binding >> map (rpair NoSyn);
+
+val for_params =
+ Scan.optional (@{keyword "for"} |-- Parse.!!! (Parse.and_list1 params >> flat)) [];
+
+in
+
+val _ =
+ Outer_Syntax.command @{command_keyword subgoal}
+ "focus on first subgoal within backward refinement"
+ (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+ for_params >> (fn ((a, b), c) =>
+ Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
+
+end;
+
+
(* proof navigation *)
fun report_back () =