author immler Thu, 17 Jan 2019 16:37:06 -0500 changeset 69682 500a7acdccd4 parent 69681 689997a8a582 child 69683 8b3458ca0762
no need for %unimportant for proofs of proposition
```--- a/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:28:07 2019 -0500
+++ b/src/HOL/Analysis/Cross3.thy	Thu Jan 17 16:37:06 2019 -0500
@@ -80,13 +80,13 @@
hide_fact (open) left_diff_distrib right_diff_distrib

proposition Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3"

-proposition  Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
-  by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3)
+proposition Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
+  by (simp add: cross3_simps) (metis (full_types) exhaust_3)

-proposition  cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
-  by%unimportant (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
+proposition cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
+  by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)

lemma  cross_components:
"(x \<times> y)\$1 = x\$2 * y\$3 - y\$2 * x\$3" "(x \<times> y)\$2 = x\$3 * y\$1 - y\$3 * x\$1" "(x \<times> y)\$3 = x\$1 * y\$2 - y\$1 * x\$2"
@@ -127,7 +127,7 @@
using exhaust_3 by (force simp add: cross3_simps)

proposition  dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)"
-  by%unimportant (force simp add: cross3_simps)
+  by (force simp add: cross3_simps)

proposition  norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
unfolding power2_norm_eq_inner power_mult_distrib```