avoid duplicate simp rules in norm_arith tactic
authorhuffman
Fri, 22 Jun 2012 15:03:41 +0200
changeset 48112 b1240319ef15
parent 48111 33414f2e82ab
child 48113 1c4500446ba4
avoid duplicate simp rules in norm_arith tactic
src/HOL/Multivariate_Analysis/Norm_Arith.thy
src/HOL/Multivariate_Analysis/normarith.ML
--- 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
 
--- 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