Tuned.
authorwebertj
Fri Oct 19 10:46:42 2012 +0200 (2012-10-19)
changeset 49961d3d2b78b1c19
parent 49934 6f7985a42889
child 49962 a8cc904a6820
Tuned.
src/HOL/Library/ListVector.thy
     1.1 --- a/src/HOL/Library/ListVector.thy	Thu Oct 18 20:59:46 2012 +0200
     1.2 +++ b/src/HOL/Library/ListVector.thy	Fri Oct 19 10:46:42 2012 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  apply(simp)
     1.5  apply(case_tac zs)
     1.6   apply(simp)
     1.7 -apply(simp add:add_assoc)
     1.8 +apply(simp add: add_assoc)
     1.9  done
    1.10  
    1.11  subsection "Inner product"
    1.12 @@ -103,13 +103,13 @@
    1.13  "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
    1.14  
    1.15  lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
    1.16 -by(simp add:iprod_def)
    1.17 +by(simp add: iprod_def)
    1.18  
    1.19  lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
    1.20 -by(simp add:iprod_def)
    1.21 +by(simp add: iprod_def)
    1.22  
    1.23  lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
    1.24 -by(simp add:iprod_def)
    1.25 +by(simp add: iprod_def)
    1.26  
    1.27  lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
    1.28  apply(induct cs arbitrary:xs)
    1.29 @@ -128,7 +128,7 @@
    1.30  apply simp
    1.31  apply(case_tac zs)
    1.32  apply (simp)
    1.33 -apply(simp add:left_distrib)
    1.34 +apply(simp add: left_distrib)
    1.35  done
    1.36  
    1.37  lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
    1.38 @@ -138,7 +138,7 @@
    1.39  apply simp
    1.40  apply(case_tac zs)
    1.41  apply (simp)
    1.42 -apply(simp add:left_diff_distrib)
    1.43 +apply(simp add: left_diff_distrib)
    1.44  done
    1.45  
    1.46  lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
    1.47 @@ -146,7 +146,7 @@
    1.48  apply simp
    1.49  apply(case_tac ys)
    1.50  apply (simp)
    1.51 -apply (simp add:right_distrib mult_assoc)
    1.52 +apply (simp add: right_distrib mult_assoc)
    1.53  done
    1.54  
    1.55 -end
    1.56 \ No newline at end of file
    1.57 +end