# HG changeset patch
# User nipkow
# Date 978429817 -3600
# Node ID 0d36ace55e5aedde4d0417f5faa64388b842cc08
# Parent  02d727c441bb620c5810d793d2fc0c134936cf14
*** empty log message ***

diff -r 02d727c441bb -r 0d36ace55e5a doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Tue Jan 02 10:35:33 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Tue Jan 02 11:03:37 2001 +0100
@@ -37,11 +37,13 @@
 @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
 @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
-@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & $\mid~\mid$\\
+@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
 @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
 @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
 @{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
-@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"}
+@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
+@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
+@{text LEAST}$~x.~P$
 \end{tabular}
 \caption{Overloaded constants in HOL}
 \label{tab:overloading}
diff -r 02d727c441bb -r 0d36ace55e5a doc-src/TutorialI/Types/document/Overloading2.tex
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Tue Jan 02 10:35:33 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Tue Jan 02 11:03:37 2001 +0100
@@ -39,11 +39,13 @@
 \isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
 \isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & $\mid~\mid$\\
+\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{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{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}
 \caption{Overloaded constants in HOL}
 \label{tab:overloading}