src/HOL/Relation.thy
changeset 56218 1c3f1f2431f9
parent 56085 3d11892ea537
child 56545 8f1e7596deb7
     1.1 --- a/src/HOL/Relation.thy	Wed Mar 19 17:06:02 2014 +0000
     1.2 +++ b/src/HOL/Relation.thy	Wed Mar 19 18:47:22 2014 +0100
     1.3 @@ -281,7 +281,7 @@
     1.4    by (fast intro: symI elim: symE)
     1.5  
     1.6  lemma symp_INF:
     1.7 -  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
     1.8 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
     1.9    by (fact sym_INTER [to_pred])
    1.10  
    1.11  lemma sym_UNION:
    1.12 @@ -289,7 +289,7 @@
    1.13    by (fast intro: symI elim: symE)
    1.14  
    1.15  lemma symp_SUP:
    1.16 -  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
    1.17 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
    1.18    by (fact sym_UNION [to_pred])
    1.19  
    1.20