doc-src/Classes/Thy/Classes.thy

   may include recursion over the syntactic structure of types.
   As a canonical example, we model product semigroups
   using our simple algebra:
 *}
 
-instantiation %quote * :: (semigroup, semigroup) semigroup
+instantiation %quote prod :: (semigroup, semigroup) semigroup
 begin
 
 definition %quote
   mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
 

     unfolding neutral_int_def mult_int_def by simp
 qed
 
 end %quote
 
-instantiation %quote * :: (monoidl, monoidl) monoidl
+instantiation %quote prod :: (monoidl, monoidl) monoidl
 begin
 
 definition %quote
   neutral_prod_def: "\<one> = (\<one>, \<one>)"
 

     unfolding neutral_int_def mult_int_def by simp
 qed
 
 end %quote
 
-instantiation %quote * :: (monoid, monoid) monoid
+instantiation %quote prod :: (monoid, monoid) monoid
 begin
 
 instance %quote proof 
   fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
   show "p \<otimes> \<one> = p"