src/HOL/Real/document/root.tex
author urbanc
Tue, 13 Dec 2005 18:11:21 +0100
changeset 18396 b3e7da94b51f
parent 12735 09a224f7d776
permissions -rw-r--r--
added a fresh_left lemma that contains all instantiation for the various atom-types.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12735
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     1
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     2
% $Id$
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     3
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     5
\usepackage{graphicx,isabelle,isabellesym,latexsym}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     6
\usepackage[latin1]{inputenc}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     7
\usepackage{pdfsetup}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     8
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
     9
\urlstyle{rm}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    10
\isabellestyle{it}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    11
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    12
\begin{document}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    13
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    14
\title{Isabelle/HOL-Real --- Higher-Order Logic with Real Numbers}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    15
\maketitle
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    16
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    17
\tableofcontents
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    18
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    19
\parindent 0pt\parskip 0.5ex
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    20
\input{session}
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    21
09a224f7d776 added HOL/Real/document/root.tex;
wenzelm
parents:
diff changeset
    22
\end{document}