# HG changeset patch
# User berghofe
# Date 831455185 -7200
# Node ID bb02e6976258041680cd2d1e4dc7086c02d340e4
# Parent  286f9b6370abfb60bd8597e571860867f69457d9
Added functions for default claset.

diff -r 286f9b6370ab -r bb02e6976258 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon May 06 15:22:33 1996 +0200
+++ b/src/Provers/classical.ML	Tue May 07 09:46:25 1996 +0200
@@ -84,6 +84,16 @@
   val inst_step_tac 	: claset -> int -> tactic
   val inst0_step_tac 	: claset -> int -> tactic
   val instp_step_tac 	: claset -> int -> tactic
+
+  val claset : claset ref
+  val AddDs 		: thm list -> unit
+  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 Fast_tac 		: int -> tactic
+
   end;
 
 
@@ -445,5 +455,21 @@
 
 fun deepen_tac cs = DEEPEN (safe_depth_tac cs);
 
+val claset = ref empty_cs;
+
+fun AddDs ts = (claset := !claset addDs ts);
+
+fun AddEs ts = (claset := !claset addEs ts);
+
+fun AddIs ts = (claset := !claset addIs ts);
+
+fun AddSDs ts = (claset := !claset addSDs ts);
+
+fun AddSEs ts = (claset := !claset addSEs ts);
+
+fun AddSIs ts = (claset := !claset addSIs ts);
+
+fun Fast_tac i = fast_tac (!claset) i; 
+
 end; 
 end;