src/HOL/HOLCF/document/root.tex
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41182 717404c7d59a
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15575
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     1
29129
9925cf74b23b scale dependency graph in document
huffman
parents: 18293
diff changeset
     2
% HOLCF/document/root.tex
15575
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     3
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     5
\usepackage{graphicx,isabelle,isabellesym,latexsym}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     6
\usepackage[only,bigsqcap]{stmaryrd}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     7
\usepackage{textcomp}
15575
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     8
\usepackage{pdfsetup}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
     9
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    10
\urlstyle{rm}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    11
\isabellestyle{it}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    12
\pagestyle{myheadings}
18293
4eaa654c92f2 reimplement Case expression pattern matching to support lazy patterns
huffman
parents: 16225
diff changeset
    13
\newcommand{\isasymas}{\textsf{as}}
4eaa654c92f2 reimplement Case expression pattern matching to support lazy patterns
huffman
parents: 16225
diff changeset
    14
\newcommand{\isasymlazy}{\isamath{\sim}}
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40945
diff changeset
    15
\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}
15575
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    16
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    17
\begin{document}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    18
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    19
\title{Isabelle/HOLCF --- Higher-Order Logic of Computable Functions}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    20
\maketitle
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    21
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    22
\tableofcontents
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    23
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    24
\begin{center}
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 29129
diff changeset
    25
  \includegraphics[scale=0.45]{session_graph}
15575
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    26
\end{center}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    27
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    28
\newpage
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    29
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    30
\renewcommand{\isamarkupheader}[1]%
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    31
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    32
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    33
\parindent 0pt\parskip 0.5ex
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    34
\input{session}
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    35
63babb1ee883 document generation for HOLCF
huffman
parents:
diff changeset
    36
\end{document}