author | haftmann |
Wed, 23 Jul 2025 13:22:58 +0200 | |
changeset 82900 | bd3685e5f883 |
parent 81570 | af49ce611685 |
permissions | -rw-r--r-- |
43141 | 1 |
\documentclass[11pt,a4paper]{article} |
73404 | 2 |
\usepackage[T1]{fontenc} |
81570 | 3 |
\usepackage{amssymb} |
43141 | 4 |
\usepackage{isabelle,isabellesym} |
47613 | 5 |
\usepackage{latexsym} |
43141 | 6 |
% this should be the last package used |
12430 | 7 |
\usepackage{pdfsetup} |
8 |
||
49191 | 9 |
% snip |
10 |
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} |
|
11 |
\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
|
12 |
|
12430 | 13 |
\urlstyle{rm} |
43141 | 14 |
\isabellestyle{it} |
12430 | 15 |
|
50043 | 16 |
\renewcommand{\isacharunderscore}{\_} |
17 |
\renewcommand{\isacharunderscorekeyword}{\_} |
|
18 |
||
43141 | 19 |
% for uniform font size |
20 |
\renewcommand{\isastyle}{\isastyleminor} |
|
21 |
||
12430 | 22 |
\begin{document} |
23 |
||
43141 | 24 |
\title{Concrete Semantics} |
54930 | 25 |
\author{Tobias Nipkow \& Gerwin Klein} |
12430 | 26 |
\maketitle |
27 |
||
61225 | 28 |
\begin{abstract} |
29 |
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}. |
|
30 |
\end{abstract} |
|
31 |
||
47602 | 32 |
\setcounter{tocdepth}{2} |
43141 | 33 |
\tableofcontents |
34 |
\newpage |
|
12430 | 35 |
|
43141 | 36 |
% generated text of all theories |
12430 | 37 |
\input{session} |
38 |
||
43141 | 39 |
\nocite{Nipkow} |
54930 | 40 |
\nocite{ConcreteSemantics} |
43141 | 41 |
|
42 |
\bibliographystyle{abbrv} |
|
12430 | 43 |
\bibliography{root} |
44 |
||
45 |
\end{document} |