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/Cartesian_Euclidean_Space.thy
changeset 69272 15e9ed5b28fb
parent 69064 5840724b1d71
child 69508 2a4c8a2a3f8e 
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:29:09 2018 +0100
@@ -229,7 +229,7 @@
 proof -
   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
     using assms unfolding invertible_def by auto
-  with `k \<noteq> 0`
+  with \<open>k \<noteq> 0\<close>
   have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
     by (simp_all add: assms matrix_scalar_ac)
   thus "invertible (k *\<^sub>R A)"
isabelle