diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Library/Product_Vector.thy
--- 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