# HG changeset patch # User haftmann # Date 1245226043 -7200 # Node ID 799aecc0df5676a58139e4a57997cbec6fe108fa # Parent 4ee7a8af1903340e5d002d9fac87a6d75540950e updated table of overloaded constants 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) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a"} \\ -@{text"*"} & @{text "('a::times) \ 'a \ 'a"} & (infixl 70) \\ -@{text div} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text mod} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text dvd} & @{text "('a::times) \ 'a \ bool"} & (infixl 50) \\ -@{text"/"} & @{text "('a::inverse) \ 'a \ 'a"} & (infixl 70) \\ -@{text"^"} & @{text "('a::power) \ nat \ 'a"} & (infixr 80) \\ -@{term abs} & @{text "('a::minus) \ 'a"} & ${\mid} x {\mid}$\\ -@{text"\"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{text"<"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{term min} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term max} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term Least} & @{text "('a::ord \ bool) \ '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(*>*) diff -r 4ee7a8af1903 -r 799aecc0df56 doc-src/TutorialI/Misc/document/appendix.tex --- a/doc-src/TutorialI/Misc/document/appendix.tex Wed Jun 17 10:07:22 2009 +0200 +++ b/doc-src/TutorialI/Misc/document/appendix.tex Wed Jun 17 10:07:23 2009 +0200 @@ -21,26 +21,23 @@ \begin{tabular}{lll} Constant & Type & Syntax \\ \hline -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\ -\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}one} \\ -\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\ -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\ -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\ -\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\ -\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & -\isa{LEAST}$~x.~P$ +\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isasymColon}zero} \\ +\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isasymColon}one} \\ +\isa{plus} & \isa{{\isacharprime}a{\isasymColon}plus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}plus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}plus} & (infixl $+$ 65) \\ +\isa{minus} & \isa{{\isacharprime}a{\isasymColon}minus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}minus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}minus} & (infixl $-$ 65) \\ +\isa{uminus} & \isa{{\isacharprime}a{\isasymColon}uminus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}uminus} & $- x$ \\ +\isa{times} & \isa{{\isacharprime}a{\isasymColon}times\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}times\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}times} & (infixl $*$ 70) \\ +\isa{divide} & \isa{{\isacharprime}a{\isasymColon}inverse\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}inverse\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}inverse} & (infixl $/$ 70) \\ +\isa{Divides{\isachardot}div} & \isa{{\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div} & (infixl $div$ 70) \\ +\isa{Divides{\isachardot}mod} & \isa{{\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div} & (infixl $mod$ 70) \\ +\isa{abs} & \isa{{\isacharprime}a{\isasymColon}abs\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}abs} & ${\mid} x {\mid}$ \\ +\isa{sgn} & \isa{{\isacharprime}a{\isasymColon}sgn\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}sgn} \\ +\isa{less{\isacharunderscore}eq} & \isa{{\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ bool} & (infixl $\le$ 50) \\ +\isa{less} & \isa{{\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ bool} & (infixl $<$ 50) \\ +\isa{top} & \isa{{\isacharprime}a{\isasymColon}top} \\ +\isa{bot} & \isa{{\isacharprime}a{\isasymColon}bot} \end{tabular} -\caption{Overloaded Constants in HOL} +\caption{Important Overloaded Constants in Main} \label{tab:overloading} \end{center} \end{table}%