src/HOL/Complex/ex/document/root.tex
author urbanc
Tue, 13 Dec 2005 18:11:21 +0100
changeset 18396 b3e7da94b51f
parent 17196 d26778f3e6dd
child 27421 7e458bd56860
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:
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     1
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     3
\usepackage[latin1]{inputenc}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     5
\usepackage{pdfsetup}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     6
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     7
\urlstyle{rm}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     8
\isabellestyle{it}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     9
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    10
\begin{document}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    11
17196
wenzelm
parents: 13957
diff changeset
    12
\title{Miscellaneous HOL-Complex Examples}
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    13
\maketitle
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    14
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    15
\tableofcontents
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    16
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    17
\parindent 0pt\parskip 0.5ex
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    18
\input{session}
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    19
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    20
\end{document}