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/ZF/int_arith.ML
changeset 78800 0b3700d31758
parent 78791 4f7dce5c1a81 
--- a/src/ZF/int_arith.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/int_arith.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -6,11 +6,11 @@
 
 signature INT_NUMERAL_SIMPROCS =
 sig
-  val inteq_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val intless_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val intle_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val int_combine_numerals_proc: Proof.context -> cterm -> thm option
-  val int_combine_numerals_prod_proc: Proof.context -> cterm -> thm option
+  val inteq_cancel_numerals_proc: Simplifier.proc
+  val intless_cancel_numerals_proc: Simplifier.proc
+  val intle_cancel_numerals_proc: Simplifier.proc
+  val int_combine_numerals_proc: Simplifier.proc
+  val int_combine_numerals_prod_proc: Simplifier.proc
 end
 
 structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
isabelle