src/Pure/goal.ML

 struct
 
 (* managing goal states *)
 
 (*
-  ----------------- (init)
-  Goal C ==> Goal C
+  ------------ (init)
+  C ==> Goal C
 *)
 fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
 
 (*
   A ==> ... ==> Goal C

 
 (*
   Goal C
   ------ (finish)
     C
-*)  
+*)
 fun finish th =
   (case Thm.nprems_of th of
     0 => conclude th
   | n => raise THM ("Proof failed.\n" ^
       Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
 
 
 (* prove_raw -- minimal checks, no normalization *)
 
-fun prove_raw thy goal tac =  
+fun prove_raw thy goal tac =
   (case SINGLE tac (init (Thm.cterm_of thy goal)) of
     SOME th => finish th
   | NONE => raise ERROR_MESSAGE "Tactic failed.");
 
 

     if 1 <= i andalso i <= n then
       if n = 1 then tac st else SELECT tac i st
     else Seq.empty
   end;
 
-
 end;
 
 structure BasicGoal: BASIC_GOAL = Goal;
 open BasicGoal;