diff -r 4ee7a8af1903 -r 799aecc0df56 doc-src/TutorialI/Misc/appendix.thy
--- a/doc-src/TutorialI/Misc/appendix.thy	Wed Jun 17 10:07:22 2009 +0200
+++ b/doc-src/TutorialI/Misc/appendix.thy	Wed Jun 17 10:07:23 2009 +0200
@@ -1,6 +1,6 @@
-(*<*)
-theory appendix imports Main begin;
-(*>*)
+(*<*)theory appendix
+imports Main
+begin(*>*)
 
 text{*
 \begin{table}[htbp]
@@ -8,31 +8,26 @@
 \begin{tabular}{lll}
 Constant & Type & Syntax \\
 \hline
-@{text 0} & @{text "'a::zero"} \\
-@{text 1} & @{text "'a::one"} \\
-@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
-@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{text"/"}  & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
-@{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 [source] 0} & @{typeof [show_sorts] "0"} \\
+@{term [source] 1} & @{typeof [show_sorts] "1"} \\
+@{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\
+@{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
+@{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
+@{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
+@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
+@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
+@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
+@{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
+@{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
+@{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
+@{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\
+@{term [source] top} & @{typeof [show_sorts] "top"} \\
+@{term [source] bot} & @{typeof [show_sorts] "bot"}
 \end{tabular}
-\caption{Overloaded Constants in HOL}
+\caption{Important Overloaded Constants in Main}
 \label{tab:overloading}
 \end{center}
 \end{table}
 *}
 
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)