src/Pure/goal.ML
changeset 17983 89103008502f
parent 17980 788836292b1a
child 17986 0450847646c3
     1.1 --- a/src/Pure/goal.ML	Fri Oct 21 18:17:00 2005 +0200
     1.2 +++ b/src/Pure/goal.ML	Fri Oct 21 18:20:29 2005 +0200
     1.3 @@ -36,8 +36,8 @@
     1.4  (* managing goal states *)
     1.5  
     1.6  (*
     1.7 -  ----------------- (init)
     1.8 -  Goal C ==> Goal C
     1.9 +  ------------ (init)
    1.10 +  C ==> Goal C
    1.11  *)
    1.12  fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
    1.13  
    1.14 @@ -56,7 +56,7 @@
    1.15    Goal C
    1.16    ------ (finish)
    1.17      C
    1.18 -*)  
    1.19 +*)
    1.20  fun finish th =
    1.21    (case Thm.nprems_of th of
    1.22      0 => conclude th
    1.23 @@ -67,7 +67,7 @@
    1.24  
    1.25  (* prove_raw -- minimal checks, no normalization *)
    1.26  
    1.27 -fun prove_raw thy goal tac =  
    1.28 +fun prove_raw thy goal tac =
    1.29    (case SINGLE tac (init (Thm.cterm_of thy goal)) of
    1.30      SOME th => finish th
    1.31    | NONE => raise ERROR_MESSAGE "Tactic failed.");
    1.32 @@ -157,7 +157,6 @@
    1.33      else Seq.empty
    1.34    end;
    1.35  
    1.36 -
    1.37  end;
    1.38  
    1.39  structure BasicGoal: BASIC_GOAL = Goal;