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/Tools/nat_arith.ML
changeset 82643 f1c14af17591
parent 82641 d22294b20573 
--- a/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:34 2025 +0200
@@ -19,7 +19,7 @@
 
 fun move_to_front ctxt path = Conv.every_conv
     [Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
-     Conv.arg_conv (Raw_Simplifier.rewrite_wrt ctxt false norm_rules)]
+     Conv.arg_conv (Simplifier.rewrite_wrt ctxt false norm_rules)]
 
 fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
       add_atoms (@{thm nat_arith.add1}::path) x #>
isabelle