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/IMP/Collecting.thy
changeset 80914 d97fdabd9e2b
parent 69712 dc85b5b3a532 
--- a/src/HOL/IMP/Collecting.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/Collecting.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,10 +9,10 @@
 subsubsection "The generic Step function"
 
 notation
-  sup (infixl "\<squnion>" 65) and
-  inf (infixl "\<sqinter>" 70) and
-  bot ("\<bottom>") and
-  top ("\<top>")
+  sup (infixl \<open>\<squnion>\<close> 65) and
+  inf (infixl \<open>\<sqinter>\<close> 70) and
+  bot (\<open>\<bottom>\<close>) and
+  top (\<open>\<top>\<close>)
 
 context
   fixes f :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
isabelle