|
1
|
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:
|