--- 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