--- a/src/HOL/Multivariate_Analysis/Determinants.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Sun Aug 18 19:59:19 2013 +0200
@@ -917,7 +917,7 @@
{fix v w
{fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
note th0 = this
- have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
+ have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this