src/HOL/ZF/document/root.tex
author paulson
Wed, 04 Jul 2007 13:56:26 +0200
changeset 23563 42f2f90b51a6
parent 19203 778507520684
child 36862 952b2b102a0a
permissions -rw-r--r--
simplified a proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     1
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     2
% $Id$
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     3
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     5
\usepackage{isabelle,isabellesym}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     6
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     7
% this should be the last package used
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     8
\usepackage{pdfsetup}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     9
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    10
% urls in roman style, theory text in math-similar italics
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    11
\urlstyle{rm}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    12
\isabellestyle{it}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    13
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    14
\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    15
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    16
\begin{document}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    17
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    18
\title{ZF}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    19
\author{Steven Obua}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    20
\maketitle
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    21
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    22
%\tableofcontents
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    23
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    24
\parindent 0pt\parskip 0.5ex
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    25
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    26
\input{session}
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    27
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    28
\end{document}