tuned whitespace;
authorwenzelm
Mon, 01 Oct 2012 20:16:37 +0200
changeset 49676 882aa078eeae
parent 49675 d9c2fb37d92a
child 49677 c4e2762a265c
tuned whitespace;
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 .