# HG changeset patch
# User paulson
# Date 967198535 -7200
# Node ID 772ac061bd762a4956f612b0ebf14b0c121d0112
# Parent  87b460d72e80f9c0d6d695ec3565c2eab9479acc
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML

diff -r 87b460d72e80 -r 772ac061bd76 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Aug 24 12:39:42 2000 +0200
+++ b/src/HOL/Set.ML	Fri Aug 25 12:15:35 2000 +0200
@@ -19,13 +19,13 @@
 by (Asm_full_simp_tac 1);
 qed "CollectD";
 
-val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
+val [prem] = Goal "(!!x. (x:A) = (x:B)) ==> A = B";
 by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
 by (rtac Collect_mem_eq 1);
 by (rtac Collect_mem_eq 1);
 qed "set_ext";
 
-val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
+val [prem] = Goal "(!!x. P(x)=Q(x)) ==> {x. P(x)} = {x. Q(x)}";
 by (rtac (prem RS ext RS arg_cong) 1);
 qed "Collect_cong";
 
@@ -557,6 +557,7 @@
 \    (UN x:A. C(x)) = (UN x:B. D(x))";
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "UN_cong";
+Addcongs [UN_cong];
 
 
 section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
@@ -591,6 +592,7 @@
 \    (INT x:A. C(x)) = (INT x:B. D(x))";
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "INT_cong";
+Addcongs [INT_cong];
 
 
 section "Union";
diff -r 87b460d72e80 -r 772ac061bd76 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Aug 24 12:39:42 2000 +0200
+++ b/src/HOL/UNITY/Union.ML	Fri Aug 25 12:15:35 2000 +0200
@@ -8,8 +8,6 @@
 From Misra's Chapter 5: Asynchronous Compositions of Programs
 *)
 
-Addcongs [UN_cong, INT_cong];
-
 
 (** SKIP **)