Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/normarith.ML
changeset 82967 73af47bc277c
parent 81954 6f2bcdfa9a19 
--- a/src/HOL/Analysis/normarith.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Analysis/normarith.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -386,7 +386,7 @@
 
   fun init_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
-    addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus},
+    |> Simplifier.add_simps ([(*@{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 ctxt
    then_conv nnf_conv ctxt
isabelle