--- a/src/HOL/Library/Product_Vector.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Vector.thy Mon Jul 06 22:57:34 2015 +0200
@@ -25,7 +25,8 @@
lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
unfolding scaleR_prod_def by simp
-instance proof
+instance
+proof
fix a b :: real and x y :: "'a \<times> 'b"
show "scaleR a (x + y) = scaleR a x + scaleR a y"
by (simp add: prod_eq_iff scaleR_right_distrib)
@@ -58,7 +59,8 @@
shows "open S"
using assms unfolding open_prod_def by fast
-instance proof
+instance
+proof
show "open (UNIV :: ('a \<times> 'b) set)"
unfolding open_prod_def by auto
next
@@ -277,7 +279,8 @@
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
-instance proof
+instance
+proof
fix x y :: "'a \<times> 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
unfolding dist_prod_def prod_eq_iff by simp
@@ -406,7 +409,8 @@
lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
unfolding norm_prod_def by simp
-instance proof
+instance
+proof
fix r :: real and x y :: "'a \<times> 'b"
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_prod_def
@@ -510,7 +514,8 @@
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
unfolding inner_prod_def by simp
-instance proof
+instance
+proof
fix r :: real
fix x y z :: "'a::real_inner \<times> 'b::real_inner"
show "inner x y = inner y x"