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/HOLCF/Fix.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/HOLCF/Fix.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Fix.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -48,11 +48,11 @@
 
 text \<open>Binder syntax for \<^term>\<open>fix\<close>\<close>
 
-abbreviation fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "\<mu> " 10)
+abbreviation fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder \<open>\<mu> \<close> 10)
   where "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
 
 notation (ASCII)
-  fix_syn  (binder "FIX " 10)
+  fix_syn  (binder \<open>FIX \<close> 10)
 
 text \<open>Properties of \<^term>\<open>fix\<close>\<close>
isabelle