--- a/src/Provers/classical.ML Mon Jun 17 16:50:08 1996 +0200
+++ b/src/Provers/classical.ML Mon Jun 17 16:50:38 1996 +0200
@@ -93,6 +93,7 @@
val AddSDs : thm list -> unit
val AddSEs : thm list -> unit
val AddSIs : thm list -> unit
+ val Delrules : thm list -> unit
val Step_tac : int -> tactic
val Fast_tac : int -> tactic
val Best_tac : int -> tactic
@@ -552,6 +553,8 @@
fun AddSIs ts = (claset := !claset addSIs ts);
+fun Delrules ts = (claset := !claset delrules ts);
+
(*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
fun Step_tac i = step_tac (!claset) i;