tuned;
authorwenzelm
Tue Jan 30 23:53:46 2001 +0100 (2001-01-30)
changeset 11004af8008e4de96
parent 11003 ee0838d89deb
child 11005 86f662ba3c3f
tuned;
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Unix/Unix.thy	Tue Jan 30 18:57:24 2001 +0100
     1.2 +++ b/src/HOL/Unix/Unix.thy	Tue Jan 30 23:53:46 2001 +0100
     1.3 @@ -975,7 +975,7 @@
     1.4    performed by @{term user1} alone.  Note that this holds for any
     1.5    @{term path} given, the particular @{term bogus_path} is not
     1.6    required here.
     1.7 -*}  (* FIXME The overall structure of the proof is as follows \dots *)
     1.8 +*}
     1.9  
    1.10  lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
    1.11    invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path"