src/HOL/IMP/document/root.tex
author bulwahn
Fri, 07 Sep 2012 14:15:46 +0200
changeset 49193 0067d83414c8
parent 49191 3601bf546775
child 50043 e8af18896060
permissions -rw-r--r--
clearer names for functions in Quickcheck's narrowing engine
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     1
\documentclass[11pt,a4paper]{article}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     2
\usepackage{isabelle,isabellesym}
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents: 47602
diff changeset
     3
\usepackage{latexsym}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     4
% this should be the last package used
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     5
\usepackage{pdfsetup}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     6
49191
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
     7
% snip
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
     8
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
     9
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 43141
diff changeset
    10
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    11
\urlstyle{rm}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    12
\isabellestyle{it}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    13
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    14
% for uniform font size
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    15
\renewcommand{\isastyle}{\isastyleminor}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    16
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    17
\begin{document}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    18
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    19
\title{Concrete Semantics}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    20
\author{TN \& GK}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    21
\maketitle
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    22
47602
3d44790b5ab0 reorganised IMP
nipkow
parents: 45246
diff changeset
    23
\setcounter{tocdepth}{2}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    24
\tableofcontents
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    25
\newpage
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    26
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    27
% generated text of all theories
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    28
\input{session}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    29
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    30
\nocite{Nipkow}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    31
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    32
\bibliographystyle{abbrv}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    33
\bibliography{root}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    34
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    35
\end{document}