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\>::\ "{}'a\ set\ \mbox{$\Rightarrow$}\ ('a\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"{}\\ |
|
8 syntax\\ |
|
9 \>"{}\mbox{$\varepsilon$}Ball"{}\>::\ "{}pttrn\ \mbox{$\Rightarrow$}\ 'a\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"{}\>\>\>\>\>("{}(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"{}\ 10)\\ |
|
10 translations\\ |
|
11 \>\>"{}\mbox{$\forall$}x\mbox{$\in$}A.\ P"{}\ \mbox{$=$}\mbox{$=$}\ "{}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} |