diff -r 78a82c37b4b2 -r 484559628038 src/HOL/UNITY/Comp/AllocBase.thy --- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jun 18 16:17:51 2015 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jun 19 15:55:22 2015 +0200 @@ -17,7 +17,7 @@ "tokens [] = 0" | "tokens (x#xs) = x + tokens xs" -abbreviation (input) "bag_of \ multiset_of" +abbreviation (input) "bag_of \ mset" lemma setsum_fun_mono [rule_format]: "!!f :: nat=>nat.