src/HOL/HOLCF/IOA/NTP/Multiset.thy
changeset 80914 d97fdabd9e2b
parent 67613 ce654b0e6d69
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -13,7 +13,7 @@
 
 consts
 
-  emptym :: "'a multiset"                        ("{|}")
+  emptym :: "'a multiset"                        (\<open>{|}\<close>)
   addm   :: "['a multiset, 'a] => 'a multiset"
   delm   :: "['a multiset, 'a] => 'a multiset"
   countm :: "['a multiset, 'a => bool] => nat"