--- a/src/HOL/Unix/Unix.thy Thu Apr 29 11:05:13 2010 +0200
+++ b/src/HOL/Unix/Unix.thy Thu Apr 29 16:53:08 2010 +0200
@@ -358,7 +358,7 @@
read:
"access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
root \<midarrow>(Read uid text path)\<rightarrow> root" |
- write:
+ "write":
"access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
@@ -436,7 +436,7 @@
case read
with root' show ?thesis by cases auto
next
- case write
+ case "write"
with root' show ?thesis by cases auto
next
case chmod