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