equal
deleted
inserted
replaced
840 The following invariant over the root file-system describes the |
840 The following invariant over the root file-system describes the |
841 bogus situation in an abstract manner: located at a certain @{term |
841 bogus situation in an abstract manner: located at a certain @{term |
842 path} within the file-system is a non-empty directory that is |
842 path} within the file-system is a non-empty directory that is |
843 neither owned nor writable by @{term user\<^isub>1}. |
843 neither owned nor writable by @{term user\<^isub>1}. |
844 *} |
844 *} |
845 |
|
846 |
|
847 |
845 |
848 definition |
846 definition |
849 "invariant root path = |
847 "invariant root path = |
850 (\<exists>att dir. |
848 (\<exists>att dir. |
851 access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
849 access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |