--- a/src/HOL/Library/Product_Vector.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/Product_Vector.thy Thu Jan 22 14:51:08 2015 +0100
@@ -538,4 +538,8 @@
end
+lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
+ by (cases x, simp)+
+
+
end