# HG changeset patch
# User wenzelm
# Date 1126018892 -7200
# Node ID 9888b0c8b2aafe281a012feb43ff96d74b745b4d
# Parent  1fe83f912bd6fac249e269a9246583211b79ab6c
updated;

diff -r 1fe83f912bd6 -r 9888b0c8b2aa doc-src/AxClass/Group/document/Group.tex
--- a/doc-src/AxClass/Group/document/Group.tex	Tue Sep 06 17:00:00 2005 +0200
+++ b/doc-src/AxClass/Group/document/Group.tex	Tue Sep 06 17:01:32 2005 +0200
@@ -124,42 +124,42 @@
 \ \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{finally}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
@@ -191,12 +191,12 @@
 \ \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \ \ \isacommand{also}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
@@ -206,7 +206,7 @@
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{finally}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
@@ -282,7 +282,7 @@
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -308,11 +308,11 @@
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
@@ -472,7 +472,7 @@
 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof