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"