1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Fri May 01 15:28:40 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Fri May 01 16:06:59 2020 +0200
     1.3 @@ -20,7 +20,10 @@
     1.4  struct
     1.5  (**)
     1.6  
     1.7 -(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)
     1.8 +(*
     1.9 +  check tactics (input by the user, mostly) for applicability
    1.10 +  and determine as much of the result of the tactic as possible initially.
    1.11 +*)
    1.12  fun check (Tactic.Check_Postcond pI) (_, (p, p_)) =
    1.13        if member op = [Pos.Pbl, Pos.Met] p_                  
    1.14        then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))