# HG changeset patch
# User haftmann
# Date 1331980518 -3600
# Node ID 144d94446378df605226d7291e9bd2e36ee24732
# Parent  d54cea5b64e4e26eb339dfdf48d382206db9b39d
spelt out missing colemmas

diff -r d54cea5b64e4 -r 144d94446378 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Mar 17 08:00:18 2012 +0100
+++ b/src/HOL/Relation.thy	Sat Mar 17 11:35:18 2012 +0100
@@ -276,13 +276,17 @@
   "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
   by (fast intro: symI elim: symE)
 
-(* FIXME thm sym_INTER [to_pred] *)
+lemma symp_INF:
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
+  by (fact sym_INTER [to_pred])
 
 lemma sym_UNION:
   "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
   by (fast intro: symI elim: symE)
 
-(* FIXME thm sym_UNION [to_pred] *)
+lemma symp_SUP:
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
+  by (fact sym_UNION [to_pred])
 
 
 subsubsection {* Antisymmetry *}