- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically
\input{intro.tex}
\input{syntax.tex}
\input{pure.tex}
\input{Generic.tex}
\input{Quick_Reference.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: