# HG changeset patch
# User wenzelm
# Date 1308394195 -7200
# Node ID f67364f35789faf8eea5ba1595c843e347006164
# Parent  224006e5ac466ca457ff592ce7973c172a0b37bc
tuned text;

diff -r 224006e5ac46 -r f67364f35789 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Jun 18 12:37:42 2011 +0200
+++ b/src/HOL/Unix/Unix.thy	Sat Jun 18 12:49:55 2011 +0200
@@ -847,7 +847,7 @@
   The following invariant over the root file-system describes the
   bogus situation in an abstract manner: located at a certain @{term
   path} within the file-system is a non-empty directory that is
-  neither owned and nor writable by @{term user\<^isub>1}.
+  neither owned nor writable by @{term user\<^isub>1}.
 *}
 
 definition