--- a/doc-src/Classes/Thy/Classes.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy Thu Mar 26 20:08:55 2009 +0100
@@ -458,7 +458,7 @@
of monoids for lists:
*}
-interpretation %quote list_monoid!: monoid append "[]"
+interpretation %quote list_monoid: monoid append "[]"
proof qed auto
text {*
@@ -473,7 +473,7 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
-interpretation %quote list_monoid!: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" where
"monoid.pow_nat append [] = replicate"
proof -
interpret monoid append "[]" ..