src/HOL/ex/document/root.tex
author bauerg
Thu, 28 Apr 2005 17:08:08 +0200
changeset 15871 e524119dbf19
parent 12509 b461efcfc886
child 19024 80eb6640f3d5
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11585
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
     1
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
     2
% $Id$
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
     3
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
12023
wenzelm
parents: 11823
diff changeset
     5
\usepackage{isabelle,isabellesym}
12509
b461efcfc886 \usepackage[latin1]{inputenc};
wenzelm
parents: 12357
diff changeset
     6
\usepackage[latin1]{inputenc}
11823
5a3fcd84e55e guillemot syntax;
wenzelm
parents: 11592
diff changeset
     7
\usepackage[english]{babel}
12357
f7fa60115e4e \usepackage{textcomp};
wenzelm
parents: 12105
diff changeset
     8
\usepackage{textcomp}
12023
wenzelm
parents: 11823
diff changeset
     9
\usepackage{pdfsetup}
11585
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    10
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    11
\urlstyle{rm}
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    12
\isabellestyle{it}
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    13
15871
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    14
\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    15
\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    16
\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    17
\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    18
\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    19
\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    20
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    21
e524119dbf19 *** empty log message ***
bauerg
parents: 12509
diff changeset
    22
11585
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    23
\begin{document}
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    24
11592
wenzelm
parents: 11585
diff changeset
    25
\title{Miscellaneous HOL Examples}
11585
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    26
\maketitle
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    27
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    28
\tableofcontents
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    29
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    30
\parindent 0pt\parskip 0.5ex
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    31
\input{session}
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    32
12105
wenzelm
parents: 12023
diff changeset
    33
\bibliographystyle{abbrv}
wenzelm
parents: 12023
diff changeset
    34
\bibliography{root}
wenzelm
parents: 12023
diff changeset
    35
11585
35a79fd062f7 document setup;
wenzelm
parents:
diff changeset
    36
\end{document}