src/HOL/UNITY/document/root.tex
author wenzelm
Tue, 22 Mar 2011 13:32:20 +0100
changeset 42048 afd11ca8e018
parent 17159 d5060118122e
child 73404 299f6a8faccc
permissions -rw-r--r--
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     1
\documentclass[10pt,a4paper,twoside]{article}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     2
\usepackage{graphicx}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     3
\usepackage{latexsym,theorem}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     5
\usepackage{pdfsetup}\urlstyle{rm}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     6
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     7
\begin{document}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     8
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
     9
\pagestyle{headings}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    10
\pagenumbering{arabic}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    11
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    12
\title{The UNITY Formalism}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    13
\author{Sidi Ehmety and Lawrence C. Paulson}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    14
\maketitle
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    15
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    16
\tableofcontents
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    17
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    18
\begin{center}
17159
d5060118122e tuned size of included graph;
wenzelm
parents: 14150
diff changeset
    19
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    20
\end{center}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    21
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    22
\newpage
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    23
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    24
\parindent 0pt\parskip 0.5ex
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    25
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    26
\input{session}
9a23e4eb5eb3 A document for UNITY
paulson
parents:
diff changeset
    27
\end{document}