changeset 47215 | ca516aa5b6ce |
parent 47175 | 6b906beec36f |
child 49077 | 154f25a162e3 |
--- a/src/HOL/Unix/Unix.thy Fri Mar 30 13:12:02 2012 +0200 +++ b/src/HOL/Unix/Unix.thy Fri Mar 30 15:25:47 2012 +0200 @@ -845,7 +845,7 @@ -definition invariant where +definition "invariant root path = (\<exists>att dir. access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>