src/Pure/Isar/proof.ML
changeset 6853 80f88b762816
parent 6848 3d82756e1af5
child 6871 01866edde713
equal deleted inserted replaced
6852:fe39a3054d82 6853:80f88b762816
   396   end;
   396   end;
   397 
   397 
   398 
   398 
   399 (* solve goal *)
   399 (* solve goal *)
   400 
   400 
   401 fun REV_RANGE _ [] = all_tac
   401 fun RANGE [] _ = all_tac
   402   | REV_RANGE k (tac :: tacs) = tac k THEN REV_RANGE (k - 1) tacs;
   402   | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
   403 
   403 
   404 fun solve_goal rule tacs state =
   404 fun solve_goal rule tacs state =
   405   let
   405   let
   406     val rev_tacs = rev tacs;
       
   407     val n = length rev_tacs - 1;
       
   408 
       
   409     val (_, (result, (facts, thm))) = find_goal 0 state;
   406     val (_, (result, (facts, thm))) = find_goal 0 state;
   410     val thms' = FIRSTGOAL (rtac rule THEN' (fn i => REV_RANGE (i + n) rev_tacs)) thm;
   407     val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm;
   411   in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
   408   in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
   412 
   409 
   413 
   410 
   414 
   411 
   415 (*** structured proof commands ***)
   412 (*** structured proof commands ***)