Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix reference to dist_def
authorhuffman
Thu, 28 May 2009 22:54:57 -0700
changeset 31293 198eae6f5a35
parent 31292 d24b2692562f
child 31294 79a40605efce
child 31336 e17f13cd1280
child 31359 0c4ec2867a4e
fix reference to dist_def
src/HOL/Library/normarith.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/normarith.ML	Thu May 28 22:53:23 2009 -0700
+++ b/src/HOL/Library/normarith.ML	Thu May 28 22:54:57 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_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 dist_vector_def}, @{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
isabelle