| changeset 81091 | c007e6d9941d |
| parent 81011 | 6d34c2bedaa3 |
| child 81145 | c9f1e926d4ed |
--- a/src/CCL/Set.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/CCL/Set.thy Tue Oct 01 20:39:16 2024 +0200 @@ -19,8 +19,6 @@ syntax "_Coll" :: "[idt, o] \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>) -syntax_consts - Collect translations "{x. P}" == "CONST Collect(\<lambda>x. P)"