1.1 --- a/doc-src/TutorialI/Misc/appendix.thy	Wed Jun 17 10:07:22 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/appendix.thy	Wed Jun 17 10:07:23 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*<*)
     1.5 -theory appendix imports Main begin;
     1.6 -(*>*)
     1.7 +(*<*)theory appendix
     1.8 +imports Main
     1.9 +begin(*>*)
    1.10  
    1.11  text{*
    1.12  \begin{table}[htbp]
    1.13 @@ -8,31 +8,26 @@
    1.14  \begin{tabular}{lll}
    1.15  Constant & Type & Syntax \\
    1.16  \hline
    1.17 -@{text 0} & @{text "'a::zero"} \\
    1.18 -@{text 1} & @{text "'a::one"} \\
    1.19 -@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
    1.20 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
    1.21 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
    1.22 -@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.23 -@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.24 -@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.25 -@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.26 -@{text"/"}  & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.27 -@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
    1.28 -@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
    1.29 -@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.30 -@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.31 -@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.32 -@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.33 -@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.34 -@{text LEAST}$~x.~P$
    1.35 +@{term [source] 0} & @{typeof [show_sorts] "0"} \\
    1.36 +@{term [source] 1} & @{typeof [show_sorts] "1"} \\
    1.37 +@{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\
    1.38 +@{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
    1.39 +@{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
    1.40 +@{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
    1.41 +@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
    1.42 +@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
    1.43 +@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
    1.44 +@{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
    1.45 +@{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
    1.46 +@{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
    1.47 +@{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\
    1.48 +@{term [source] top} & @{typeof [show_sorts] "top"} \\
    1.49 +@{term [source] bot} & @{typeof [show_sorts] "bot"}
    1.50  \end{tabular}
    1.51 -\caption{Overloaded Constants in HOL}
    1.52 +\caption{Important Overloaded Constants in Main}
    1.53  \label{tab:overloading}
    1.54  \end{center}
    1.55  \end{table}
    1.56  *}
    1.57  
    1.58 -(*<*)
    1.59 -end
    1.60 -(*>*)
    1.61 +(*<*)end(*>*)