Addition of Safe_step_tac
authorpaulson
Tue, 18 Jun 1996 16:36:04 +0200
changeset 1814 89f8d4a88cca
parent 1813 23bda45846a2
child 1815 cd3ffa5f1e31
Addition of Safe_step_tac
src/Provers/classical.ML
--- 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;