# HG changeset patch
# User wenzelm
# Date 1272552788 -7200
# Node ID 7cc639e20cb2061ce5c3cc83c4ec72390a00a12b
# Parent  bd4e2821482a63cdf5b54e79cf52c3fcb95ac147
avoid clash with keyword 'write';

diff -r bd4e2821482a -r 7cc639e20cb2 src/HOL/TLA/Memory/MemoryParameters.thy
--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Apr 29 11:05:13 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Apr 29 16:53:08 2010 +0200
@@ -12,7 +12,7 @@
 begin
 
 (* the memory operations *)
-datatype memOp = read Locs | write Locs Vals
+datatype memOp = read Locs | "write" Locs Vals
 
 consts
   (* memory locations and contents *)
diff -r bd4e2821482a -r 7cc639e20cb2 src/HOL/Unix/Unix.thy
--- 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