author | kuncar |
Fri, 23 Mar 2012 14:34:50 +0100 | |
changeset 47099 | 56adbf5bcc82 |
parent 47098 | bab1c32c201e |
child 47100 | f8f788c8b7f3 |
--- 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>