1.1 --- a/src/HOL/Relation.thy	Sat Mar 17 08:00:18 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Mar 17 11:35:18 2012 +0100
     1.3 @@ -276,13 +276,17 @@
     1.4    "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
     1.5    by (fast intro: symI elim: symE)
     1.6  
     1.7 -(* FIXME thm sym_INTER [to_pred] *)
     1.8 +lemma symp_INF:
     1.9 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
    1.10 +  by (fact sym_INTER [to_pred])
    1.11  
    1.12  lemma sym_UNION:
    1.13    "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
    1.14    by (fast intro: symI elim: symE)
    1.15  
    1.16 -(* FIXME thm sym_UNION [to_pred] *)
    1.17 +lemma symp_SUP:
    1.18 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
    1.19 +  by (fact sym_UNION [to_pred])
    1.20  
    1.21  
    1.22  subsubsection {* Antisymmetry *}