\documentclass[11pt,a4paper]{article}+
−
\usepackage{amsmath,amsthm}+
−
\usepackage{CookBook/generated/isabelle,CookBook/generated/isabellesym}+
−
+
−
+
−
% Cross references to other manuals:+
−
\usepackage{xr}+
−
\externaldocument[I-]{implementation}+
−
\newcommand{\impref}[1]{\ref{I-#1}}+
−
\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]}+
−
\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]}+
−
+
−
+
−
% further packages required for unusual symbols (see also+
−
% isabellesym.sty), use only when needed+
−
+
−
%\usepackage{amssymb}+
−
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,+
−
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,+
−
  %\<triangleq>, \<yen>, \<lozenge>+
−
+
−
%\usepackage[greek,english]{babel}+
−
  %option greek for \<euro>+
−
  %option english (default language) for \<guillemotleft>, \<guillemotright>+
−
+
−
%\usepackage[latin1]{inputenc}+
−
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,+
−
  %\<threesuperior>, \<threequarters>, \<degree>+
−
+
−
%\usepackage[only,bigsqcap]{stmaryrd}+
−
  %for \<Sqinter>+
−
+
−
%\usepackage{eufrak}+
−
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)+
−
+
−
%\usepackage{textcomp}+
−
  %for \<cent>, \<currency>+
−
+
−
% this should be the last package used+
−
\usepackage{pdfsetup}+
−
+
−
\urlstyle{rm}+
−
\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text+
−
\renewcommand{\isastyle}{\isastyleminor}% use same formatting for txt and text+
−
\isadroptag{theory}+
−
+
−
\newenvironment{readmore}{\makebox[0pt][r]{\fbox{\textbf{Read More}}~~}\it}{}+
−
+
−
\newtheorem{exercise}{Exercise}[section]+
−
+
−
+
−
\begin{document}+
−
+
−
\title{The Isabelle Programmer's Cookbook (fragment)}+
−
\author{Alexander Krauss}+
−
\maketitle+
−
+
−
\tableofcontents+
−
+
−
% sane default for proof documents+
−
\parindent 0pt\parskip 0.5ex+
−
+
−
% generated text of all theories+
−
\input{CookBook/generated/CookBook}+
−
\newpage\section{Recipes}+
−
\input{CookBook/generated/NamedThms}+
−
+
−
\newpage+
−
\bibliographystyle{abbrv}+
−
\bibliography{manual,cookbook}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−