src/HOL/IMP/document/root.tex
author nipkow
Wed, 01 Jun 2011 21:35:34 +0200
changeset 43141 11fce8564415
parent 12546 0c90e581379f
child 45246 4fbeabee6487
permissions -rw-r--r--
Replacing old IMP with new Semantics material
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}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     3
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     4
% further packages required for unusual symbols (see also
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     5
% isabellesym.sty), use only when needed
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     6
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     7
%\usepackage{amssymb}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     8
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
     9
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    10
  %\<triangleq>, \<yen>, \<lozenge>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    11
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    12
%\usepackage[greek,english]{babel}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    13
  %option greek for \<euro>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    14
  %option english (default language) for \<guillemotleft>, \<guillemotright>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    15
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    16
%\usepackage[latin1]{inputenc}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    17
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    18
  %\<threesuperior>, \<threequarters>, \<degree>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    19
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    20
%\usepackage[only,bigsqcap]{stmaryrd}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    21
  %for \<Sqinter>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    22
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    23
%\usepackage{eufrak}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    24
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    25
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    26
%\usepackage{textcomp}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    27
  %for \<cent>, \<currency>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    28
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    29
% this should be the last package used
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    30
\usepackage{pdfsetup}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    31
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    32
% urls in roman style, theory text in math-similar italics
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    33
\urlstyle{rm}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    34
\isabellestyle{it}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    35
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    36
\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    37
\newcommand{\isasymSKIP}{\CMD{skip}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    38
\newcommand{\isasymIF}{\CMD{if}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    39
\newcommand{\isasymTHEN}{\CMD{then}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    40
\newcommand{\isasymELSE}{\CMD{else}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    41
\newcommand{\isasymWHILE}{\CMD{while}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    42
\newcommand{\isasymDO}{\CMD{do}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    43
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    44
% for uniform font size
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    45
\renewcommand{\isastyle}{\isastyleminor}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    46
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    47
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    48
\begin{document}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    49
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    50
\title{Concrete Semantics}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    51
\author{TN \& GK}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    52
\maketitle
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    53
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    54
\tableofcontents
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    55
\newpage
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    56
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    57
% generated text of all theories
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    58
\input{session}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    59
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    60
\nocite{Nipkow}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    61
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    62
% optional bibliography
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    63
\bibliographystyle{abbrv}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    64
\bibliography{root}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    65
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    66
\end{document}