Addition of Safe_step_tac
authorpaulson
Tue Jun 18 16:36:04 1996 +0200 (1996-06-18)
changeset 181489f8d4a88cca
parent 1813 23bda45846a2
child 1815 cd3ffa5f1e31
Addition of Safe_step_tac
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Tue Jun 18 16:27:04 1996 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Jun 18 16:36:04 1996 +0200
     1.3 @@ -94,6 +94,7 @@
     1.4    val AddSEs		: thm list -> unit
     1.5    val AddSIs		: thm list -> unit
     1.6    val Delrules		: thm list -> unit
     1.7 +  val Safe_step_tac	: int -> tactic
     1.8    val Step_tac 		: int -> tactic
     1.9    val Fast_tac 		: int -> tactic
    1.10    val Best_tac 		: int -> tactic
    1.11 @@ -557,6 +558,8 @@
    1.12  
    1.13  (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
    1.14  
    1.15 +fun Safe_step_tac i = safe_step_tac (!claset) i; 
    1.16 +
    1.17  fun Step_tac i = step_tac (!claset) i; 
    1.18  
    1.19  fun Fast_tac i = fast_tac (!claset) i;