1 \documentclass[11pt,a4paper]{article} |
1 \documentclass[11pt,a4paper]{report} |
2 \usepackage{amsmath,amsthm} |
2 \usepackage{amsmath,amsthm} |
3 \usepackage{isabelle,isabellesym} |
3 \usepackage{isabelle} |
4 |
4 \usepackage{isabellesym} |
|
5 \usepackage{charter} |
|
6 \usepackage[pdftex]{graphicx} |
5 |
7 |
6 % Cross references to other manuals: |
8 % Cross references to other manuals: |
7 \usepackage{xr} |
9 \usepackage{xr} |
8 \externaldocument{implementation} |
10 \externaldocument[I-]{implementation} |
9 \newcommand{\impref}[1]{\ref{I-#1}} |
11 \newcommand{\impref}[1]{\ref{I-#1}} |
|
12 \newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]} |
|
13 \newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]} |
10 |
14 |
11 |
|
12 % further packages required for unusual symbols (see also |
|
13 % isabellesym.sty), use only when needed |
|
14 |
|
15 %\usepackage{amssymb} |
|
16 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
|
17 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
|
18 %\<triangleq>, \<yen>, \<lozenge> |
|
19 |
|
20 %\usepackage[greek,english]{babel} |
|
21 %option greek for \<euro> |
|
22 %option english (default language) for \<guillemotleft>, \<guillemotright> |
|
23 |
|
24 %\usepackage[latin1]{inputenc} |
|
25 %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>, |
|
26 %\<threesuperior>, \<threequarters>, \<degree> |
|
27 |
|
28 %\usepackage[only,bigsqcap]{stmaryrd} |
|
29 %for \<Sqinter> |
|
30 |
|
31 %\usepackage{eufrak} |
|
32 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) |
|
33 |
|
34 %\usepackage{textcomp} |
|
35 %for \<cent>, \<currency> |
|
36 |
|
37 % this should be the last package used |
|
38 \usepackage{pdfsetup} |
15 \usepackage{pdfsetup} |
39 |
16 |
40 \urlstyle{rm} |
17 \urlstyle{rm} |
41 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
18 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
42 \renewcommand{\isastyle}{\isastyleminor}% use same formatting for txt and text |
19 \renewcommand{\isastyle}{\isastyleminor}% use same formatting for txt and text |
43 \isadroptag{theory} |
20 \isadroptag{theory} |
44 |
21 |
|
22 \newenvironment{readmore} |
|
23 {\makebox[0pt][r]{\fbox{\textbf{Read More}}~~}\it}{} |
45 |
24 |
46 \newtheorem{exercise}{Exercise}[section] |
25 \newtheorem{exercise}{Exercise}[section] |
47 |
26 |
48 |
27 |
49 \begin{document} |
28 \begin{document} |
50 |
29 |
51 \title{The Isabelle Programmer's Cookbook (fragment)} |
30 \title{\mbox{}\\[-10ex] |
52 \author{Alexander Krauss} |
31 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
|
32 The Isabelle Programmer's Cookbook (fragment)} |
|
33 \author{with contributions by:\\[2ex] |
|
34 \begin{tabular}{l} |
|
35 Alexander Krauss\\ |
|
36 Jeremy Dawson\\ |
|
37 Stefan Berghofer |
|
38 \end{tabular}} |
53 \maketitle |
39 \maketitle |
54 |
40 |
55 \tableofcontents |
41 \tableofcontents |
56 |
42 |
57 % sane default for proof documents |
43 % sane default for proof documents |
58 \parindent 0pt\parskip 0.5ex |
44 \parindent 0pt\parskip 0.5ex |
59 |
45 |
60 % generated text of all theories |
46 % generated text of all theories |
61 \input{session} |
47 \input{session} |
62 |
48 |
63 % optional bibliography |
49 \newpage |
64 %\bibliographystyle{abbrv} |
50 \bibliographystyle{abbrv} |
65 %\bibliography{root} |
51 \bibliography{manul,cookbook} |
66 |
52 |
67 \end{document} |
53 \end{document} |
68 |
54 |
69 %%% Local Variables: |
55 %%% Local Variables: |
70 %%% mode: latex |
56 %%% mode: latex |