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