# HG changeset patch
# User nipkow
# Date 1513883704 -3600
# Node ID d0ca4e41883952e6c8bccbe30062f940fda45f0b
# Parent  b2d2584ace51a1b4b5daaba8a8c4ac5bd5f98d60
tuned op's

diff -r b2d2584ace51 -r d0ca4e418839 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 19:55:41 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 20:15:04 2017 +0100
@@ -2282,7 +2282,7 @@
   assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
   shows "path_connected {x. P(norm(x - a))}"
 proof -
-  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
+  have "{x. P(norm(x - a))} = op+ a ` {x. P(norm x)}"
     by force
   moreover have "path_connected {x::'N. P(norm x)}"
   proof -