--- a/src/HOL/Unix/Unix.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Unix/Unix.thy Fri Sep 20 19:51:08 2024 +0200
@@ -336,7 +336,7 @@
\<close>
inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
- ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
+ (\<open>_ \<midarrow>_\<rightarrow> _\<close> [90, 1000, 90] 100)
where
read:
"root \<midarrow>(Read uid text path)\<rightarrow> root"
@@ -475,7 +475,7 @@
running processes over a finite amount of time.
\<close>
-inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" (\<open>_ \<Midarrow>_\<Rightarrow> _\<close> [90, 1000, 90] 100)
where
nil: "root \<Midarrow>[]\<Rightarrow> root"
| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"