changeset 63882 | 018998c00003 |
parent 63410 | 9789ccc2a477 |
child 64267 | b9a1486e79be |
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Sep 14 22:07:11 2016 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Sep 15 11:48:20 2016 +0200 @@ -14,7 +14,7 @@ abbreviation (input) tokens :: "nat list \<Rightarrow> nat" where - "tokens \<equiv> listsum" + "tokens \<equiv> sum_list" abbreviation (input) "bag_of \<equiv> mset"