--- a/src/HOL/Unix/Unix.thy Wed Aug 29 16:25:35 2012 +0900
+++ b/src/HOL/Unix/Unix.thy Thu Aug 30 13:03:03 2012 +0900
@@ -952,7 +952,7 @@
with tr obtain opt where root': "root' = update (path_of x) opt root"
by cases auto
show ?thesis
- proof (rule prefix_cases)
+ proof (rule prefixeq_cases)
assume "path_of x \<parallel> path"
with inv root'
have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"
@@ -960,7 +960,7 @@
with inv show "invariant root' path"
by (simp only: invariant_def)
next
- assume "path_of x \<le> path"
+ assume "prefixeq (path_of x) path"
then obtain ys where path: "path = path_of x @ ys" ..
show ?thesis
@@ -997,7 +997,7 @@
by (simp only: invariant_def access_def)
qed
next
- assume "path < path_of x"
+ assume "prefix path (path_of x)"
then obtain y ys where path: "path_of x = path @ y # ys" ..
obtain dir' where