--- a/CookBook/document/root.tex	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,157 +0,0 @@
-\documentclass[11pt,a4paper]{report}
-\usepackage[latin1]{inputenc}
-\usepackage{amsmath,amsthm}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{charter}
-\usepackage[pdftex]{graphicx}
-\usepackage{proof}
-\usepackage{rail}
-\usepackage{url}
-\usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
-\usepackage{lineno}
-\usepackage{xcolor}
-\usepackage{framed}
-\usepackage{boxedminipage}
-\usepackage{mathpartir}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
-\renewcommand{\isastyleminor}{\tt\slshape}%
-\renewcommand{\isastyle}{\small\tt\slshape}%
-\isadroptag{theory}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% For cross references to the 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}]}
-\externaldocument[R-]{isar-ref}
-\newcommand{\isarref}[1]{\ref{R-#1}}
-\newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
-\newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% sane default for proof documents
-\parindent 0pt
-\parskip 0.6ex
-\abovecaptionskip 1mm
-\belowcaptionskip 10mm
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\hyphenation{Isabelle}
-\renewcommand{\isasymiota}{}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% to work around a problem with \isanewline
-\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for exercises, comments and readmores
-\newtheorem{exercise}{Exercise}[section]
-\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
-
-\newcommand{\readmoremarginpar}[1]%
-{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
-
-\newenvironment{leftrightbar}{%
-\def\FrameCommand##1{\vrule width 2pt \hspace{8pt}##1\hspace{8pt}\vrule width 2pt}%
-\MakeFramed {\advance\hsize-\width \FrameRestore}}%
-{\endMakeFramed}
-
-
-\newenvironment{readmore}%
-{\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% this is to draw a gray box around code
-%(FIXME redefine pagebreak so that it includes a \smallskip)
-\newenvironment{graybox}
-{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}}
-{\smallskip\endMakeFramed}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% this hack is for getting rid of the ML {* ... *} 
-% scaffolding around function definitions
-\newenvironment{vanishML}{%
-\renewcommand{\isacommand}[1]{}%
-\renewcommand{\isacharverbatimopen}{}%
-\renewcommand{\isacharverbatimclose}{}}{}
-
-\isakeeptag{TutorialML}
-\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
-\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for code that has line numbers
-\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers}
-
-\isakeeptag{linenos}
-\renewcommand{\isataglinenos}{\begin{linenos}}
-\renewcommand{\endisataglinenos}{\end{linenos}}
-
-% should only be used in ML code
-\isakeeptag{linenosgray}
-\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
-\renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}
-
-\isakeeptag{gray}
-\renewcommand{\isataggray}{\begin{graybox}}
-\renewcommand{\endisataggray}{\end{graybox}}
-
-\isakeeptag{small}
-\renewcommand{\isatagsmall}{\begingroup\small}
-\renewcommand{\endisatagsmall}{\endgroup}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\renewenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\small\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for {*  *} in antiquotations
-\newcommand{\isasymverbopen}{\isacharverbatimopen}
-\newcommand{\isasymverbclose}{\isacharverbatimclose}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% since * cannot be used in text {*...*} 
-\newenvironment{tabularstar}[2]
-{\begin{tabular*}{#1}{#2}}{\end{tabular*}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% short hands
-\def\simpleinductive{\isacommand{simple\isacharunderscore{}inductive}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{document}
-
-\title{\mbox{}\\[-10ex]
-       \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
-       The Isabelle Programming Tutorial (draft)}
-
-\author{by Christian Urban with contributions from:\\[2ex] 
-        \begin{tabular}{r@{\hspace{1.8mm}}l}
-        Stefan & Berghofer\\
-        Sascha & Böhme\\
-        Jeremy & Dawson\\
-        Alexander & Krauss\\ 
-        \end{tabular}}
-
-\maketitle
-\tableofcontents
-
-% generated text of all theories
-\input{session}
-
-\newpage
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: