--- a/src/Provers/classical.ML Tue Jun 18 16:27:04 1996 +0200
+++ b/src/Provers/classical.ML Tue Jun 18 16:36:04 1996 +0200
@@ -94,6 +94,7 @@
val AddSEs : thm list -> unit
val AddSIs : thm list -> unit
val Delrules : thm list -> unit
+ val Safe_step_tac : int -> tactic
val Step_tac : int -> tactic
val Fast_tac : int -> tactic
val Best_tac : int -> tactic
@@ -557,6 +558,8 @@
(*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
+fun Safe_step_tac i = safe_step_tac (!claset) i;
+
fun Step_tac i = step_tac (!claset) i;
fun Fast_tac i = fast_tac (!claset) i;