doc-src/IsarAdvanced/Classes/Thy/Classes.thy

 consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
 
 text {*
   \noindent The connection to the type system is done by means
   of a primitive axclass
-*}
+*} setup %invisible {* Sign.add_path "foo" *}
 
 axclass %quote idem < type
-  idem: "f (f x) = f x"
+  idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
 
 text {* \noindent together with a corresponding interpretation: *}
 
-interpretation %quote idem_class':    (* FIXME proper prefix? *)
+interpretation %quote idem_class:
   idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
 proof qed (rule idem)
 
 text {*
   \noindent This gives you at hand the full power of the Isabelle module system;

   the same operations as for genuinely algebraic types.
   In such a case, we simply can do a particular interpretation
   of monoids for lists:
 *}
 
-class_interpretation %quote list_monoid: monoid [append "[]"]
+interpretation %quote list_monoid!: monoid append "[]"
   proof qed auto
 
 text {*
   \noindent This enables us to apply facts on monoids
   to lists, e.g. @{thm list_monoid.neutl [no_vars]}.

 
 primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-class_interpretation %quote list_monoid: monoid [append "[]"] where
+interpretation %quote list_monoid!: monoid append "[]" where
   "monoid.pow_nat append [] = replicate"
 proof -
-  class_interpret monoid [append "[]"] ..
+  interpret monoid append "[]" ..
   show "monoid.pow_nat append [] = replicate"
   proof
     fix n
     show "monoid.pow_nat append [] n = replicate n"
       by (induct n) auto