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