src/HOL/Hyperreal/ex/document/root.tex
author paulson
Sun, 14 Jul 2002 15:14:43 +0200
changeset 13356 c9cfe1638bf2
parent 13029 84e4ba7fb033
permissions -rw-r--r--
improved presentation markup
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     1
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     3
\usepackage[latin1]{inputenc}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     5
\usepackage{pdfsetup}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     6
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     7
\urlstyle{rm}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     8
\isabellestyle{it}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
     9
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    10
\begin{document}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    11
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    12
\title{Miscellaneous HOL-Hyperreal Examples}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    13
\maketitle
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    14
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    15
\tableofcontents
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    16
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    17
\parindent 0pt\parskip 0.5ex
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    18
\input{session}
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    19
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents:
diff changeset
    20
\end{document}