diff -r 42f2619adfd7 -r 610d17d32b9e src/Tools/8bit/doc/Set2a.tex --- a/src/Tools/8bit/doc/Set2a.tex Wed Nov 05 15:36:40 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article} -\begin{document} -{\isamode -\begin{tabbing} -xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex} -consts\\ -\>Ball\>::\ "{}'a\ set\ \mbox{$\Rightarrow$}\ ('a\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"{}\\ -syntax\\ -\>"{}\mbox{$\varepsilon$}Ball"{}\>::\ "{}pttrn\ \mbox{$\Rightarrow$}\ 'a\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"{}\>\>\>\>\>("{}(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"{}\ 10)\\ -translations\\ -\>\>"{}\mbox{$\forall$}x\mbox{$\in$}A.\ P"{}\ \mbox{$=$}\mbox{$=$}\ "{}Ball\ A\ (\mbox{$\lambda$}x.\ P)"{}\\ -defs\\ -\ \ \ \ \ Ball\_def\>\>"{}Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"{}\\ -\\ - -\end{tabbing}} -\end{document}