src/Provers/classical.ML
changeset 1814 89f8d4a88cca
parent 1807 3ff66483a8d4
child 1927 6f97cb16e453
     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;