src/HOL/Analysis/Linear_Algebra.thy
changeset 68074 8d50467f7555
parent 68073 fad29d2a17a5
child 68224 1f7308050349
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu May 03 15:07:14 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu May 03 16:17:44 2018 +0200
     1.3 @@ -917,7 +917,7 @@
     1.4      and bg: "bilinear g"
     1.5      and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
     1.6    shows "f = g"
     1.7 -  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
     1.8 +  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
     1.9  
    1.10  subsection \<open>Infinity norm\<close>
    1.11