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