author | nipkow |
Tue, 22 Sep 2015 14:31:22 +0200 | |
changeset 61225 | 1a690dce8cfc |
parent 54930 | f2ec28292479 |
child 73404 | 299f6a8faccc |
permissions | -rw-r--r-- |
43141 | 1 |
\documentclass[11pt,a4paper]{article} |
2 |
\usepackage{isabelle,isabellesym} |
|
47613 | 3 |
\usepackage{latexsym} |
43141 | 4 |
% this should be the last package used |
12430 | 5 |
\usepackage{pdfsetup} |
6 |
||
49191 | 7 |
% snip |
8 |
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} |
|
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 | 11 |
\urlstyle{rm} |
43141 | 12 |
\isabellestyle{it} |
12430 | 13 |
|
50043 | 14 |
\renewcommand{\isacharunderscore}{\_} |
15 |
\renewcommand{\isacharunderscorekeyword}{\_} |
|
16 |
||
43141 | 17 |
% for uniform font size |
18 |
\renewcommand{\isastyle}{\isastyleminor} |
|
19 |
||
12430 | 20 |
\begin{document} |
21 |
||
43141 | 22 |
\title{Concrete Semantics} |
54930 | 23 |
\author{Tobias Nipkow \& Gerwin Klein} |
12430 | 24 |
\maketitle |
25 |
||
61225 | 26 |
\begin{abstract} |
27 |
This document presents formalizations of the semantics of a simple imperative programming language together with a number of applications: a compiler, type systems, various program analyses and abstract interpreters. These theories form the basis of the book \emph{Concrete Semantics with Isabelle/HOL} by Nipkow and Klein \cite{NipkowK2014}. |
|
28 |
\end{abstract} |
|
29 |
||
47602 | 30 |
\setcounter{tocdepth}{2} |
43141 | 31 |
\tableofcontents |
32 |
\newpage |
|
12430 | 33 |
|
43141 | 34 |
% generated text of all theories |
12430 | 35 |
\input{session} |
36 |
||
43141 | 37 |
\nocite{Nipkow} |
54930 | 38 |
\nocite{ConcreteSemantics} |
43141 | 39 |
|
40 |
\bibliographystyle{abbrv} |
|
12430 | 41 |
\bibliography{root} |
42 |
||
43 |
\end{document} |