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/Unix/Unix.thy
changeset 81142 6ad2c917dd2e
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Unix/Unix.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -336,7 +336,7 @@
 \<close>
 
 inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
-  (\<open>_ \<midarrow>_\<rightarrow> _\<close> [90, 1000, 90] 100)
+  (\<open>(\<open>open_block notation=\<open>mixfix transition\<close>\<close>_ \<midarrow>_\<rightarrow> _)\<close> [90, 1000, 90] 100)
   where
     read:
       "root \<midarrow>(Read uid text path)\<rightarrow> root"
@@ -475,7 +475,8 @@
   running processes over a finite amount of time.
 \<close>
 
-inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"  (\<open>_ \<Midarrow>_\<Rightarrow> _\<close> [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>mixfix transitions\<close>\<close>_ \<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''"
isabelle