|
1826
|
1 |
\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
|
|
|
2 |
\begin{document}
|
|
|
3 |
{\isamode
|
|
|
4 |
\begin{tabbing}
|
|
|
5 |
xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
|
|
|
6 |
consts\\
|
|
|
7 |
\>Ball\>::\ "\mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ (\mbox{$\alpha$}\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"\\
|
|
|
8 |
syntax\\
|
|
|
9 |
\>"@Ball"\>::\ "pttrn\ \mbox{$\Rightarrow$}\ \mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"\>\>\>\>\>("(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"\ 10)\\
|
|
|
10 |
translations\\
|
|
|
11 |
\>\>"\mbox{$\forall$}x\mbox{$\in$}A.\ P"\ \mbox{$\equiv$}\ "Ball\ A\ (\mbox{$\lambda$}x.\ P)"\\
|
|
|
12 |
defs\\
|
|
|
13 |
\ \ \ \ \ Ball\_def\>\>"Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"\\
|
|
|
14 |
\\
|
|
|
15 |
|
|
|
16 |
\end{tabbing}}
|
|
|
17 |
\end{document}
|