diff -r 843dba3d307a -r c007e6d9941d src/CCL/Set.thy --- 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] \ 'a set" (\(\indent=1 notation=\mixfix Collect\\{_./ _})\) -syntax_consts - Collect translations "{x. P}" == "CONST Collect(\x. P)"