| changeset 81091 | c007e6d9941d |
| parent 81090 | 843dba3d307a |
| child 81102 | 739b99d0911a |
--- a/src/HOL/Library/FSet.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Library/FSet.thy Tue Oct 01 20:39:16 2024 +0200 @@ -166,8 +166,6 @@ syntax "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>) -syntax_consts - finsert translations "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}"