*** empty log message ***
authornipkow
Mon Jan 29 19:24:17 2001 +0100 (2001-01-29)
changeset 109949429f2e7d16a
parent 10993 883248dcf3f8
child 10995 ef0b521698b7
*** empty log message ***
doc-src/TutorialI/Misc/appendix.thy
doc-src/TutorialI/Misc/document/appendix.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Misc/appendix.thy	Mon Jan 29 19:24:17 2001 +0100
     1.3 @@ -0,0 +1,37 @@
     1.4 +(*<*)
     1.5 +theory appendix = Main:;
     1.6 +(*>*)
     1.7 +
     1.8 +text{*
     1.9 +\begin{table}[htbp]
    1.10 +\begin{center}
    1.11 +\begin{tabular}{lll}
    1.12 +Constant & Type & Syntax \\
    1.13 +\hline
    1.14 +@{term 0} & @{text "'a::zero"} \\
    1.15 +@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
    1.16 +@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
    1.17 +@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
    1.18 +@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.19 +@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.20 +@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.21 +@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.22 +@{text"/"}  & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    1.23 +@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
    1.24 +@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
    1.25 +@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.26 +@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.27 +@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.28 +@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.29 +@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.30 +@{text LEAST}$~x.~P$
    1.31 +\end{tabular}
    1.32 +\caption{Overloaded Constants in HOL}
    1.33 +\label{tab:overloading}
    1.34 +\end{center}
    1.35 +\end{table}
    1.36 +*}
    1.37 +
    1.38 +(*<*)
    1.39 +end
    1.40 +(*>*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Misc/document/appendix.tex	Mon Jan 29 19:24:17 2001 +0100
     2.3 @@ -0,0 +1,38 @@
     2.4 +%
     2.5 +\begin{isabellebody}%
     2.6 +\def\isabellecontext{appendix}%
     2.7 +%
     2.8 +\begin{isamarkuptext}%
     2.9 +\begin{table}[htbp]
    2.10 +\begin{center}
    2.11 +\begin{tabular}{lll}
    2.12 +Constant & Type & Syntax \\
    2.13 +\hline
    2.14 +\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
    2.15 +\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
    2.16 +\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
    2.17 +\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
    2.18 +\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
    2.19 +\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
    2.20 +\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
    2.21 +\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
    2.22 +\isa{{\isacharslash}}  & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
    2.23 +\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
    2.24 +\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
    2.25 +\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
    2.26 +\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
    2.27 +\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
    2.28 +\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
    2.29 +\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
    2.30 +\isa{LEAST}$~x.~P$
    2.31 +\end{tabular}
    2.32 +\caption{Overloaded Constants in HOL}
    2.33 +\label{tab:overloading}
    2.34 +\end{center}
    2.35 +\end{table}%
    2.36 +\end{isamarkuptext}%
    2.37 +\end{isabellebody}%
    2.38 +%%% Local Variables:
    2.39 +%%% mode: latex
    2.40 +%%% TeX-master: "root"
    2.41 +%%% End: