src/HOL/Unix/Unix.thy

   of the file-system configuration. This is expressed as an inductive relation
   (although there is no actual recursion involved here).
 \<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"
       if "access root path uid {Readable} = Some (Val (att, text))"
   | "write":

   modeled inductively as follows. In a sense, this relation describes the
   cumulative effect of the sequence of system-calls issued by a number of
   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''"
 
 text \<open>