# HG changeset patch
# User paulson
# Date 835023038 -7200
# Node ID 3ff66483a8d4b50327ad3281374d5349ffcc2839
# Parent  12708740f58d854a85df20f6791bd930fd5fc2c4
Now exports Delrules

diff -r 12708740f58d -r 3ff66483a8d4 src/Provers/classical.ML
--- 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;