1.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
     1.6  apply (induct_tac "l", simp)
     1.7 - apply (simp add: plus_ac0)
     1.8 + apply (simp add: add_ac)
     1.9  done
    1.10  
    1.11  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    1.12 @@ -80,7 +80,7 @@
    1.13        (\<Sum>i: A Int lessThan (length l). {# l!i #})"
    1.14  apply (rule_tac xs = l in rev_induct, simp)
    1.15  apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    1.16 -                 bag_of_sublist_lemma plus_ac0)
    1.17 +                 bag_of_sublist_lemma add_ac)
    1.18  done
    1.19  
    1.20