added an explicit file containing references in the Implementation manual (should be replaced by antiquotations)
\documentclass[11pt,a4paper]{report}\usepackage{amsmath,amsthm}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{charter}\usepackage[pdftex]{graphicx}% 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}]}\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}% sane default for proof documents\parindent 0pt\parskip 0.6ex% for comments on the margin\newcommand{\readmoremarginpar}[1]%{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}\newenvironment{readmore}%{\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}\newtheorem{exercise}{Exercise}[section]\begin{document}\title{\mbox{}\\[-10ex] \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] The Isabelle Programmer's Cookbook (fragment)}\author{with contributions by:\\[2ex] \begin{tabular}{l} Alexander Krauss\\ Jeremy Dawson\\ Stefan Berghofer \end{tabular}}\maketitle\tableofcontents% generated text of all theories\input{session}\newpage\bibliographystyle{abbrv}\bibliography{cookbook}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: