author | nipkow |
Thu, 19 Apr 2012 20:19:13 +0200 | |
changeset 47613 | e72e44cee6f2 |
parent 47602 | 3d44790b5ab0 |
child 48170 | 9b41d34450e8 |
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 |
||
47613 | 7 |
\usepackage{latexsym} |
8 |
||
43141 | 9 |
%\usepackage{amssymb} |
10 |
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
|
11 |
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
|
12 |
%\<triangleq>, \<yen>, \<lozenge> |
|
13 |
||
14 |
%\usepackage[greek,english]{babel} |
|
15 |
%option greek for \<euro> |
|
16 |
%option english (default language) for \<guillemotleft>, \<guillemotright> |
|
17 |
||
18 |
%\usepackage[latin1]{inputenc} |
|
19 |
%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>, |
|
20 |
%\<threesuperior>, \<threequarters>, \<degree> |
|
21 |
||
22 |
%\usepackage[only,bigsqcap]{stmaryrd} |
|
23 |
%for \<Sqinter> |
|
24 |
||
25 |
%\usepackage{eufrak} |
|
26 |
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) |
|
27 |
||
28 |
%\usepackage{textcomp} |
|
29 |
%for \<cent>, \<currency> |
|
30 |
||
31 |
% this should be the last package used |
|
12430 | 32 |
\usepackage{pdfsetup} |
33 |
||
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
|
34 |
\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
|
35 |
|
43141 | 36 |
% urls in roman style, theory text in math-similar italics |
12430 | 37 |
\urlstyle{rm} |
43141 | 38 |
\isabellestyle{it} |
12430 | 39 |
|
43141 | 40 |
% for uniform font size |
41 |
\renewcommand{\isastyle}{\isastyleminor} |
|
42 |
||
12430 | 43 |
|
44 |
\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
|
45 |
\openisaverbatimout fragments |
12430 | 46 |
|
43141 | 47 |
\title{Concrete Semantics} |
48 |
\author{TN \& GK} |
|
12430 | 49 |
\maketitle |
50 |
||
47602 | 51 |
\setcounter{tocdepth}{2} |
43141 | 52 |
\tableofcontents |
53 |
\newpage |
|
12430 | 54 |
|
43141 | 55 |
% generated text of all theories |
12430 | 56 |
\input{session} |
57 |
||
43141 | 58 |
\nocite{Nipkow} |
59 |
||
60 |
% optional bibliography |
|
61 |
\bibliographystyle{abbrv} |
|
12430 | 62 |
\bibliography{root} |
63 |
||
64 |
\end{document} |