| changeset 81090 | 843dba3d307a |
| parent 81019 | dd59daa3c37a |
| child 81091 | c007e6d9941d |
--- a/src/HOL/Library/FSet.thy Mon Sep 30 22:57:45 2024 +0200 +++ b/src/HOL/Library/FSet.thy Mon Sep 30 23:32:26 2024 +0200 @@ -165,7 +165,7 @@ by simp syntax - "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>) + "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>) syntax_consts finsert translations