# HG changeset patch
# User paulson
# Date 940610019 -7200
# Node ID 5bfde29f1dbbbdb85ad3ecdab45ce3c4b886c9b1
# Parent  86be2946bb0b354d38a294fbbff2b22be700057f
new default simprules for UN and INT

diff -r 86be2946bb0b -r 5bfde29f1dbb src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Oct 22 18:26:46 1999 +0200
+++ b/src/HOL/equalities.ML	Fri Oct 22 18:33:39 1999 +0200
@@ -877,6 +877,8 @@
      "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
      "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
      "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
+     "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
+     "(UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)",
      "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
 
 val INT_simps = map prover
@@ -887,6 +889,8 @@
      "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
      "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
      "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
+     "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
+     "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
      "(INT x:f``A. B x)    = (INT a:A. B(f a))"];