src/HOL/IMP/document/root.tex
author haftmann
Wed, 23 Jul 2025 13:22:58 +0200
changeset 82900 bd3685e5f883
parent 81570 af49ce611685
permissions -rw-r--r--
eliminate code drop: declarations where none needed
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}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 61225
diff changeset
     2
\usepackage[T1]{fontenc}
81570
af49ce611685 proper LaTeX setup (amending 41b387d47739);
wenzelm
parents: 73404
diff changeset
     3
\usepackage{amssymb}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     4
\usepackage{isabelle,isabellesym}
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents: 47602
diff changeset
     5
\usepackage{latexsym}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     6
% this should be the last package used
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     7
\usepackage{pdfsetup}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     8
49191
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
     9
% snip
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
    10
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
3601bf546775 tuned latex
nipkow
parents: 49003
diff changeset
    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
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    13
\urlstyle{rm}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    14
\isabellestyle{it}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    15
50043
e8af18896060 fixed underscores
nipkow
parents: 49191
diff changeset
    16
\renewcommand{\isacharunderscore}{\_}
e8af18896060 fixed underscores
nipkow
parents: 49191
diff changeset
    17
\renewcommand{\isacharunderscorekeyword}{\_}
e8af18896060 fixed underscores
nipkow
parents: 49191
diff changeset
    18
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    19
% for uniform font size
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    20
\renewcommand{\isastyle}{\isastyleminor}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    21
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    22
\begin{document}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    23
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    24
\title{Concrete Semantics}
54930
f2ec28292479 minimized class dependency, updated references
nipkow
parents: 50043
diff changeset
    25
\author{Tobias Nipkow \& Gerwin Klein}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    26
\maketitle
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    27
61225
1a690dce8cfc tuned references
nipkow
parents: 54930
diff changeset
    28
\begin{abstract}
1a690dce8cfc tuned references
nipkow
parents: 54930
diff changeset
    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}.
1a690dce8cfc tuned references
nipkow
parents: 54930
diff changeset
    30
\end{abstract}
1a690dce8cfc tuned references
nipkow
parents: 54930
diff changeset
    31
47602
3d44790b5ab0 reorganised IMP
nipkow
parents: 45246
diff changeset
    32
\setcounter{tocdepth}{2}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    33
\tableofcontents
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    34
\newpage
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    35
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    36
% generated text of all theories
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    37
\input{session}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    38
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    39
\nocite{Nipkow}
54930
f2ec28292479 minimized class dependency, updated references
nipkow
parents: 50043
diff changeset
    40
\nocite{ConcreteSemantics}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    41
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    42
\bibliographystyle{abbrv}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    43
\bibliography{root}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    44
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    45
\end{document}