doc-src/Classes/Thy/Classes.thy

 
 instantiation %quote * :: (semigroup, semigroup) semigroup
 begin
 
 definition %quote
-  mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
+  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)"
 
 instance %quote proof
-  fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
-  show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
+  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
     unfolding mult_prod_def by (simp add: assoc)
 qed      
 
 end %quote