src/HOL/IMP/document/root.tex
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45246 4fbeabee6487
child 47602 3d44790b5ab0
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
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
    32
\usepackage{isaverbatimwrite}
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
    33
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    34
% urls in roman style, theory text in math-similar italics
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    35
\urlstyle{rm}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    36
\isabellestyle{it}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    37
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    38
\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    39
\newcommand{\isasymSKIP}{\CMD{skip}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    40
\newcommand{\isasymIF}{\CMD{if}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    41
\newcommand{\isasymTHEN}{\CMD{then}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    42
\newcommand{\isasymELSE}{\CMD{else}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    43
\newcommand{\isasymWHILE}{\CMD{while}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    44
\newcommand{\isasymDO}{\CMD{do}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    45
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    46
% for uniform font size
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    47
\renewcommand{\isastyle}{\isastyleminor}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    48
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    49
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    50
\begin{document}
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
    51
\openisaverbatimout fragments
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    52
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    53
\title{Concrete Semantics}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    54
\author{TN \& GK}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    55
\maketitle
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    56
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    57
\tableofcontents
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    58
\newpage
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    59
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    60
% generated text of all theories
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    61
\input{session}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    62
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    63
\nocite{Nipkow}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    64
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    65
% optional bibliography
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 12546
diff changeset
    66
\bibliographystyle{abbrv}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    67
\bibliography{root}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    68
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    69
\end{document}