| changeset 78801 | 42ae6e0ecfd4 |
| parent 78099 | 4d9349989d94 |
| child 79772 | 817d33f8aa7f |
--- a/src/HOL/Finite_Set.thy Thu Oct 19 17:06:39 2023 +0200 +++ b/src/HOL/Finite_Set.thy Thu Oct 19 21:38:09 2023 +0200 @@ -24,7 +24,7 @@ end -simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close> +simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.proc\<close> declare [[simproc del: finite_Collect]]