changeset 78800 | 0b3700d31758 |
parent 78793 | 2cb027b95188 |
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Thu Oct 19 16:31:17 2023 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Thu Oct 19 17:06:39 2023 +0200 @@ -8,7 +8,7 @@ val cont_thms: term -> thm list val all_cont_thms: term -> thm list val cont_tac: Proof.context -> int -> tactic - val cont_proc: Proof.context -> cterm -> thm option + val cont_proc: Simplifier.proc end structure ContProc : CONT_PROC =