# HG changeset patch
# User wenzelm
# Date 1349115397 -7200
# Node ID 882aa078eeae5cb784f3ba0c6d84df8869fb0919
# Parent  d9c2fb37d92a356c1dc69d9ba5ae757316e98434
tuned whitespace;

diff -r d9c2fb37d92a -r 882aa078eeae src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Mon Oct 01 17:29:00 2012 +0200
+++ b/src/HOL/Unix/Unix.thy	Mon Oct 01 20:16:37 2012 +0200
@@ -1035,7 +1035,7 @@
               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
                   lookup root ((path @ [y]) @ us) \<noteq> None"
                 by cases (auto dest: access_some_lookup)
-              then show ?thesis 
+              then show ?thesis
                 by (fastforce dest!: lookup_some_append)
             qed
             finally show ?thesis .