Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Path_Connected.thy
changeset 68310 d0a7ddf5450e
parent 68296 69d680e94961
child 68532 f8b98d31ad45 
--- a/src/HOL/Analysis/Path_Connected.thy	Sun May 27 22:57:06 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon May 28 23:15:23 2018 +0100
@@ -2192,7 +2192,7 @@
       then have "norm ((x \<bullet> b) *\<^sub>R b) = norm x"
         by simp
       with b have "\<bar>x \<bullet> b\<bar> = norm x"
-        using norm_Basis by fastforce
+        using norm_Basis by (simp add: b)
       with xb show ?thesis
         apply (simp add: abs_if split: if_split_asm)
         apply (metis add.inverse_inverse real_vector.scale_minus_left xb)
isabelle