# HG changeset patch
# User immler
# Date 1547761026 18000
# Node ID 500a7acdccd4cc3c287fc830d3b74ce3766968b6
# Parent  689997a8a582ddd41d260fbbf0d9db24e048e35d
no need for %unimportant for proofs of proposition

diff -r 689997a8a582 -r 500a7acdccd4 src/HOL/Analysis/Cross3.thy
--- 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"
-  by%unimportant (simp add: cross3_simps)
+  by (simp add: cross3_simps)
 
-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