--- a/src/HOL/HOLCF/ex/Letrec.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy Fri Sep 20 19:51:08 2024 +0200
@@ -15,12 +15,12 @@
nonterminal recbinds and recbindt and recbind
syntax
- "_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
- "" :: "recbind \<Rightarrow> recbindt" ("_")
- "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
- "" :: "recbindt \<Rightarrow> recbinds" ("_")
- "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
- "_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
+ "_recbind" :: "[logic, logic] \<Rightarrow> recbind" (\<open>(2_ =/ _)\<close> 10)
+ "" :: "recbind \<Rightarrow> recbindt" (\<open>_\<close>)
+ "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" (\<open>_,/ _\<close>)
+ "" :: "recbindt \<Rightarrow> recbinds" (\<open>_\<close>)
+ "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" (\<open>_;/ _\<close>)
+ "_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" (\<open>(Letrec (_)/ in (_))\<close> 10)
syntax_consts
"_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec