resolve invariant constant name clash
authorkuncar
Fri, 23 Mar 2012 14:34:50 +0100
changeset 47099 56adbf5bcc82
parent 47098 bab1c32c201e
child 47100 f8f788c8b7f3
resolve invariant constant name clash
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>