src/Sequents/prover.ML
changeset 6054 4a4f6ad607a1
parent 4440 9ed4098074bc
child 7097 5ab37ed3d53c
equal deleted inserted replaced
6053:8a1059aa01f0 6054:4a4f6ad607a1
   104 
   104 
   105 (*tries the safe rules repeatedly before the unsafe rules. *)
   105 (*tries the safe rules repeatedly before the unsafe rules. *)
   106 fun repeat_goal_tac (Pack(safes,unsafes)) = 
   106 fun repeat_goal_tac (Pack(safes,unsafes)) = 
   107   let val restac  =    RESOLVE_THEN safes
   107   let val restac  =    RESOLVE_THEN safes
   108       and lastrestac = RESOLVE_THEN unsafes;
   108       and lastrestac = RESOLVE_THEN unsafes;
   109       fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
   109       fun gtac i = restac gtac i  
       
   110 	           ORELSE  (print_tac "" THEN lastrestac gtac i)
   110   in  gtac  end; 
   111   in  gtac  end; 
   111 
   112 
   112 
   113 
   113 (*Tries safe rules only*)
   114 (*Tries safe rules only*)
   114 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   115 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;