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/Library/Lub_Glb.thy
changeset 69597 ff784d5a5bfb
parent 69593 3dda49e08b9d 
--- a/src/HOL/Library/Lub_Glb.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/Lub_Glb.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -10,10 +10,10 @@
 
 text \<open>Thanks to suggestions by James Margetson\<close>
 
-definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
+definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl \<open>*<=\<close> 70)
   where "S *<= x = (\<forall>y\<in>S. y \<le> x)"
 
-definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
+definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl \<open><=*\<close> 70)
   where "x <=* S = (\<forall>y\<in>S. x \<le> y)"
isabelle