# HG changeset patch
# User wenzelm
# Date 1230840033 -3600
# Node ID 6cd3ac4708d248e4e1006d5a11a2afec120a615f
# Parent  d4ef21262b8f468a081376947ab451e189f769a0
crude adaption to intermediate class/locale version;

diff -r d4ef21262b8f -r 6cd3ac4708d2 doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Jan 01 20:56:23 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Jan 01 21:00:33 2009 +0100
@@ -375,8 +375,8 @@
 
 text {* \noindent together with a corresponding interpretation: *}
 
-interpretation %quote idem_class:
-  idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
+interpretation %quote idem_class':    (* FIXME proper prefix? *)
+  idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
 proof qed (rule idem)
 
 text {*
@@ -459,7 +459,7 @@
   of monoids for lists:
 *}
 
-interpretation %quote list_monoid: monoid [append "[]"]
+class_interpretation %quote list_monoid: monoid [append "[]"]
   proof qed auto
 
 text {*
@@ -474,10 +474,10 @@
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-interpretation %quote list_monoid: monoid [append "[]"] where
+class_interpretation %quote list_monoid: monoid [append "[]"] where
   "monoid.pow_nat append [] = replicate"
 proof -
-  interpret monoid [append "[]"] ..
+  class_interpret monoid [append "[]"] ..
   show "monoid.pow_nat append [] = replicate"
   proof
     fix n