1.1 --- a/src/HOL/Unix/Unix.thy	Fri Mar 23 14:29:29 2012 +0100
     1.2 +++ b/src/HOL/Unix/Unix.thy	Fri Mar 23 14:34:50 2012 +0100
     1.3 @@ -843,7 +843,9 @@
     1.4    neither owned nor writable by @{term user\<^isub>1}.
     1.5  *}
     1.6  
     1.7 -definition
     1.8 +
     1.9 +
    1.10 +definition invariant where 
    1.11    "invariant root path =
    1.12      (\<exists>att dir.
    1.13        access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>