src/HOL/Library/normarith.ML
changeset 31344 fc09ec06b89b
parent 31293 198eae6f5a35
child 31445 c8a474a919a7
--- a/src/HOL/Library/normarith.ML	Fri May 29 14:09:58 2009 -0700
+++ b/src/HOL/Library/normarith.ML	Fri May 29 15:32:33 2009 -0700
@@ -391,7 +391,7 @@
 
   fun init_conv ctxt = 
    Simplifier.rewrite (Simplifier.context ctxt 
-     (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_vector_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+     (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
    then_conv field_comp_conv 
    then_conv nnf_conv