1.1 --- a/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:35 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:40 2007 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*<*)
     1.5 -theory appendix imports Main begin;
     1.6 +theory appendix
     1.7 +imports Main
     1.8 +begin
     1.9  (*>*)
    1.10  
    1.11  text{*
    1.12 @@ -22,12 +24,10 @@
    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 min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.17 -@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.18 -@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.19 -@{text LEAST}$~x.~P$
    1.20 +%@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.21 +%@{text LEAST}$~x.~P$
    1.22  \end{tabular}
    1.23 -\caption{Overloaded Constants in HOL}
    1.24 +\caption{Algebraic symbols and operations in HOL}
    1.25  \label{tab:overloading}
    1.26  \end{center}
    1.27  \end{table}