doc-src/Classes/Thy/document/Classes.tex
changeset 35282 8fd9d555d04d
parent 34179 5490151d1052
child 37216 3165bc303f66
     1.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 14:11:03 2010 +0100
     1.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 17:02:39 2010 +0100
     1.3 @@ -641,7 +641,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \noindent The connection to the type system is done by means
     1.7 -  of a primitive axclass%
     1.8 +  of a primitive type class%
     1.9  \end{isamarkuptext}%
    1.10  \isamarkuptrue%
    1.11  \ %
    1.12 @@ -663,9 +663,8 @@
    1.13  \endisadelimquote
    1.14  %
    1.15  \isatagquote
    1.16 -\isacommand{axclass}\isamarkupfalse%
    1.17 -\ idem\ {\isacharless}\ type\isanewline
    1.18 -\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
    1.19 +\isacommand{classes}\isamarkupfalse%
    1.20 +\ idem\ {\isacharless}\ type%
    1.21  \endisatagquote
    1.22  {\isafoldquote}%
    1.23  %
    1.24 @@ -698,10 +697,7 @@
    1.25  \isatagquote
    1.26  \isacommand{interpretation}\isamarkupfalse%
    1.27  \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
    1.28 -\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
    1.29 -\isacommand{proof}\isamarkupfalse%
    1.30 -\ \isacommand{qed}\isamarkupfalse%
    1.31 -\ {\isacharparenleft}rule\ idem{\isacharparenright}%
    1.32 +\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
    1.33  \endisatagquote
    1.34  {\isafoldquote}%
    1.35  %