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/Complete_Lattices.thy
changeset 52141 eff000cab70f
parent 51540 eea5c4ca4a0e
child 52729 412c9e0381a1 
--- a/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:08 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:29 2013 +0200
@@ -751,7 +751,7 @@
   "Inter S \<equiv> \<Sqinter>S"
   
 notation (xsymbols)
-  Inter  ("\<Inter>_" [90] 90)
+  Inter  ("\<Inter>_" [900] 900)
 
 lemma Inter_eq:
   "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -934,7 +934,7 @@
   "Union S \<equiv> \<Squnion>S"
 
 notation (xsymbols)
-  Union  ("\<Union>_" [90] 90)
+  Union  ("\<Union>_" [900] 900)
 
 lemma Union_eq:
   "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
isabelle