changeset 78800 | 0b3700d31758 |
parent 70527 | 095e6459d3da |
--- a/src/Provers/Arith/combine_numerals.ML Thu Oct 19 16:31:17 2023 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Thu Oct 19 17:06:39 2023 +0200 @@ -38,7 +38,7 @@ functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): sig - val proc: Proof.context -> cterm -> thm option + val proc: Simplifier.proc end = struct