--- a/src/HOL/Unix/Unix.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Unix/Unix.thy Fri Nov 17 02:20:03 2006 +0100
@@ -166,6 +166,7 @@
Val (att, text) \<Rightarrow> att
| Env att dir \<Rightarrow> att)"
+definition
"map_attributes f file =
(case file of
Val (att, text) \<Rightarrow> Val (f att, text)
@@ -830,6 +831,7 @@
[Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
+definition
"bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
text {*