# HG changeset patch
# User haftmann
# Date 1179767498 -7200
# Node ID e7cd9719dbc2822224928a60e18404a097719890
# Parent  c722004c5a2239781a1884d05151a7d3e781dd62
min/max

diff -r c722004c5a22 -r e7cd9719dbc2 doc-src/TutorialI/Misc/document/appendix.tex
--- a/doc-src/TutorialI/Misc/document/appendix.tex	Mon May 21 19:05:37 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/appendix.tex	Mon May 21 19:11:38 2007 +0200
@@ -35,8 +35,8 @@
 \isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
 \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
 \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{Orderings{\isachardot}min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{Orderings{\isachardot}max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
 \isa{LEAST}$~x.~P$
 \end{tabular}
diff -r c722004c5a22 -r e7cd9719dbc2 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon May 21 19:05:37 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon May 21 19:11:38 2007 +0200
@@ -154,7 +154,7 @@
 \isa{{\isasymand}}, \isa{{\isasymor}}, \isa{{\isasymlongrightarrow}}, \isa{{\isacharequal}},
 \isa{{\isasymforall}}, \isa{{\isasymexists}}), the relations \isa{{\isacharequal}},
 \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations \isa{{\isacharplus}}, \isa{{\isacharminus}},
-\isa{Orderings{\isachardot}min} and \isa{Orderings{\isachardot}max}.  For example,%
+\isa{min} and \isa{max}.  For example,%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%