changeset 78793 | 2cb027b95188 |
parent 69605 | a96320074298 |
--- a/src/HOL/HOLCF/Domain_Aux.thy Tue Oct 17 18:55:29 2023 +0200 +++ b/src/HOL/HOLCF/Domain_Aux.thy Tue Oct 17 22:25:48 2023 +0200 @@ -358,6 +358,8 @@ ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close> ML_file \<open>Tools/cont_consts.ML\<close> ML_file \<open>Tools/cont_proc.ML\<close> +simproc_setup cont ("cont f") = \<open>K ContProc.cont_proc\<close> + ML_file \<open>Tools/Domain/domain_constructors.ML\<close> ML_file \<open>Tools/Domain/domain_induction.ML\<close>