doc-src/TutorialI/Ifexpr/document/root.tex
author wenzelm
Thu, 21 Sep 2000 15:58:13 +0200
changeset 10052 5fa8d8d5c852
parent 8745 13b32661dde4
permissions -rw-r--r--
renamed HOL/ex/Points to HOL/ex/Records;

\documentclass{article}
\begin{document}
xxx
\end{document}