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/int_arith.ML
changeset 80701 39cd50407f79
parent 78808 64973b03b778
child 80721 ac39d932ddfc 
--- a/src/HOL/Tools/int_arith.ML	Tue Aug 13 18:31:40 2024 +0200
+++ b/src/HOL/Tools/int_arith.ML	Tue Aug 13 18:53:24 2024 +0200
@@ -57,7 +57,8 @@
        @{thms of_int_add of_int_mult
          of_int_diff of_int_minus of_int_less_iff
          of_int_le_iff of_int_eq_iff}
-  |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
+  |> Simplifier.add_proc zero_to_of_int_zero_simproc
+  |> Simplifier.add_proc one_to_of_int_one_simproc
   |> simpset_of;
 
 val zero_one_idom_simproc =
isabelle