doc-src/TutorialI/Misc/appendix.thy

--- a/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:35 2007 +0200
+++ b/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:40 2007 +0200
@@ -1,5 +1,7 @@
 (*<*)
-theory appendix imports Main begin;
+theory appendix
+imports Main
+begin
 (*>*)
 
 text{*
@@ -22,12 +24,10 @@
 @{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 Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
-@{text LEAST}$~x.~P$
+%@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
+%@{text LEAST}$~x.~P$
 \end{tabular}
-\caption{Overloaded Constants in HOL}
+\caption{Algebraic symbols and operations in HOL}
 \label{tab:overloading}
 \end{center}
 \end{table}