--- a/src/HOL/Unix/Unix.thy Tue Jan 30 18:57:24 2001 +0100
+++ b/src/HOL/Unix/Unix.thy Tue Jan 30 23:53:46 2001 +0100
@@ -975,7 +975,7 @@
performed by @{term user1} alone. Note that this holds for any
@{term path} given, the particular @{term bogus_path} is not
required here.
-*} (* FIXME The overall structure of the proof is as follows \dots *)
+*}
lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path"