# HG changeset patch
# User huffman
# Date 1340370221 -7200
# Node ID b1240319ef158fa55fcaebdfb7c0a77cb039659c
# Parent  33414f2e82abb48178c9a32dd1f9f8929a9308a8
avoid duplicate simp rules in norm_arith tactic

diff -r 33414f2e82ab -r b1240319ef15 src/HOL/Multivariate_Analysis/Norm_Arith.thy
--- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Thu Jun 21 13:51:44 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Fri Jun 22 15:03:41 2012 +0200
@@ -108,10 +108,6 @@
   arith_simps
   add_numeral_special
   add_neg_numeral_special
-  add_0_left
-  add_0_right
-  mult_zero_left
-  mult_zero_right
   mult_1_left
   mult_1_right
 
diff -r 33414f2e82ab -r b1240319ef15 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jun 21 13:51:44 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri Jun 22 15:03:41 2012 +0200
@@ -376,7 +376,7 @@
 
   fun init_conv ctxt =
    Simplifier.rewrite (Simplifier.context ctxt
-     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
    then_conv Numeral_Simprocs.field_comp_conv
    then_conv nnf_conv