Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Relation.thy
changeset 56218 1c3f1f2431f9
parent 56085 3d11892ea537
child 56545 8f1e7596deb7 
--- a/src/HOL/Relation.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Relation.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -281,7 +281,7 @@
   by (fast intro: symI elim: symE)
 
 lemma symp_INF:
-  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
   by (fact sym_INTER [to_pred])
 
 lemma sym_UNION:
@@ -289,7 +289,7 @@
   by (fast intro: symI elim: symE)
 
 lemma symp_SUP:
-  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
   by (fact sym_UNION [to_pred])
isabelle