# HG changeset patch
# User wenzelm
# Date 980895226 -3600
# Node ID af8008e4de96304636dafa3bebe0435e9769e62b
# Parent  ee0838d89debc58048e45bb6409c35631279cedd
tuned;

diff -r ee0838d89deb -r af8008e4de96 src/HOL/Unix/Unix.thy
--- 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"