# HG changeset patch
# User haftmann
# Date 1246603894 -7200
# Node ID 0b1d807b1c2d2e8cdf0786391e34a63ddb0cd7f0
# Parent  3107b9af1fb3ba190042a8297909d21f995a29a5
restored subscripts

diff -r 3107b9af1fb3 -r 0b1d807b1c2d doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Fri Jul 03 08:44:13 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Fri Jul 03 08:51:34 2009 +0200
@@ -198,11 +198,11 @@
 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      
 
diff -r 3107b9af1fb3 -r 0b1d807b1c2d doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Fri Jul 03 08:44:13 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Fri Jul 03 08:51:34 2009 +0200
@@ -291,15 +291,15 @@
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
 \ \isacommand{proof}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{fix}\isamarkupfalse%
-\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline