
diff -r bab1c32c201e -r 56adbf5bcc82 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Mar 23 14:29:29 2012 +0100
+++ b/src/HOL/Unix/Unix.thy	Fri Mar 23 14:34:50 2012 +0100
@@ -843,7 +843,9 @@
   neither owned nor writable by @{term user\<^isub>1}.
 *}
 
-definition
+
+
+definition invariant where 
   "invariant root path =
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>




