diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/document/root.tex	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,157 @@
+\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: