src/Provers/classical.ML

   val AddEs 		: thm list -> unit
   val AddIs 		: thm list -> unit
   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
   val Deepen_tac	: int -> int -> tactic
 

 
 fun AddSEs ts = (claset := !claset addSEs ts);
 
 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; 
 
 fun Fast_tac i = fast_tac (!claset) i;