| changeset 81182 | fc5066122e68 |
| parent 81128 | 5b201b24d99b |
| child 81202 | 243f6bec771c |
--- a/src/HOL/Library/FSet.thy Fri Oct 18 11:44:05 2024 +0200 +++ b/src/HOL/Library/FSet.thy Fri Oct 18 14:20:09 2024 +0200 @@ -166,6 +166,8 @@ syntax "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>) +syntax_consts + "_fset" \<rightleftharpoons> finsert translations "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}"