src/HOL/List.thy
changeset 29223 e09c53289830
parent 28965 1de908189869
child 29270 0eade173f77e
     1.1 --- a/src/HOL/List.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -548,9 +548,9 @@
     1.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 -interpretation semigroup_append: semigroup_add ["op @"]
     1.8 +class_interpretation semigroup_append: semigroup_add ["op @"]
     1.9    proof qed simp
    1.10 -interpretation monoid_append: monoid_add ["[]" "op @"]
    1.11 +class_interpretation monoid_append: monoid_add ["[]" "op @"]
    1.12    proof qed simp+
    1.13  
    1.14  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"