# HG changeset patch
# User paulson
# Date 830940196 -7200
# Node ID c06d01f75764600b17cf90e6a10c3c7b1081cecb
# Parent  f50ec5b35937c25c253c470cd0440f24d5937f74
Provides merge_cs to support default clasets

diff -r f50ec5b35937 -r c06d01f75764 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed May 01 10:38:14 1996 +0200
+++ b/src/Provers/classical.ML	Wed May 01 10:43:16 1996 +0200
@@ -35,6 +35,7 @@
   type claset
   type netpair
   val empty_cs		: claset
+  val merge_cs		: claset * claset -> claset
   val addDs 		: claset * thm list -> claset
   val addEs 		: claset * thm list -> claset
   val addIs 		: claset * thm list -> claset
@@ -317,6 +318,22 @@
 fun cs addafter tac2  = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2);
 
 
+(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
+  Merging the term nets may look more efficient, but the rather delicate
+  treatment of priority might get muddled up.*)
+fun merge_cs
+    (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, ...},
+     CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) =
+  let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
+      val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
+      val hazIs' = gen_rems eq_thm (hazIs2,hazIs)
+      val hazEs' = gen_rems eq_thm (hazEs2,hazEs)
+  in cs addSIs safeIs'
+        addSEs safeEs'
+        addIs  hazIs'
+        addEs  hazEs'
+  end;
+
 
 (*** Simple tactics for theorem proving ***)