1.1 --- a/doc-src/TutorialI/Misc/appendix.thy	Tue Sep 18 10:44:02 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/appendix.thy	Tue Sep 18 11:06:22 2007 +0200
     1.3 @@ -1,7 +1,5 @@
     1.4  (*<*)
     1.5 -theory appendix
     1.6 -imports Main
     1.7 -begin
     1.8 +theory appendix imports Main begin;
     1.9  (*>*)
    1.10  
    1.11  text{*
    1.12 @@ -24,10 +22,12 @@
    1.13  @{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
    1.14  @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.15  @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.16 -%@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.17 -%@{text LEAST}$~x.~P$
    1.18 +@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.19 +@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.20 +@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.21 +@{text LEAST}$~x.~P$
    1.22  \end{tabular}
    1.23 -\caption{Algebraic symbols and operations in HOL}
    1.24 +\caption{Overloaded Constants in HOL}
    1.25  \label{tab:overloading}
    1.26  \end{center}
    1.27  \end{table}