# HG changeset patch
# User wenzelm
# Date 1348329356 -7200
# Node ID e87b42a26991f26753c1ee86e6b53b0e3170970d
# Parent  68796a77c42bc1ab37fa2718da77acd529615246
misc tuning;

diff -r 68796a77c42b -r e87b42a26991 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Sep 22 14:41:41 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Sep 22 17:55:56 2012 +0200
@@ -128,7 +128,8 @@
   unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
 
 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
-  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps)
+  unfolding power2_norm_eq_inner inner_simps inner_commute
+  by (auto simp add: algebra_simps)
 
 text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
 
@@ -161,7 +162,7 @@
 
 lemma setsum_clauses:
   shows "setsum f {} = 0"
-  and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
+    and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
   by (auto simp add: insert_absorb)
 
 lemma setsum_norm_le:
@@ -410,8 +411,8 @@
 
 lemma infinite_enumerate: assumes fS: "infinite S"
   shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
-unfolding subseq_def
-using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
+  unfolding subseq_def
+  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
 
 lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
   apply auto