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";