equal
deleted
inserted
replaced
|
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} |