src/HOL/UNITY/Comp/AllocBase.thy
changeset 60515 484559628038
parent 60397 f8a513fedb31
child 62430 9527ff088c15
     1.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jun 18 16:17:51 2015 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jun 19 15:55:22 2015 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    "tokens [] = 0"
     1.5  | "tokens (x#xs) = x + tokens xs"
     1.6  
     1.7 -abbreviation (input) "bag_of \<equiv> multiset_of"
     1.8 +abbreviation (input) "bag_of \<equiv> mset"
     1.9  
    1.10  lemma setsum_fun_mono [rule_format]:
    1.11       "!!f :: nat=>nat.