src/HOL/HOLCF/Domain_Aux.thy
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>