--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/tutorial.tex Wed Apr 19 11:54:39 2000 +0200
@@ -0,0 +1,78 @@
+\documentclass[11pt,a4paper]{report}
+\usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
+
+\usepackage{ttbox}
+\newcommand\ttbreak{\vskip-10pt\pagebreak[0]}
+\newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
+
+%\newtheorem{theorem}{Theorem}[section]
+\newtheorem{Exercise}{Exercise}[section]
+\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
+\newcommand{\ttlbr}{\texttt{[|}}
+\newcommand{\ttrbr}{\texttt{|]}}
+\newcommand{\ttor}{\texttt{|}}
+\newcommand{\ttall}{\texttt{!}}
+\newcommand{\ttuniquex}{\texttt{?!}}
+\newcommand{\ttEXU}{\texttt{EX!}}
+\newcommand{\ttAnd}{\texttt{!!}}
+
+\newcommand{\isasymimp}{\isasymlongrightarrow}
+\newcommand{\isasymImp}{\isasymLongrightarrow}
+\newcommand{\isasymFun}{\isasymRightarrow}
+\newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
+
+\newenvironment{isabellepar}%
+{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
+
+\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
+
+%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
+%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
+%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
+%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
+%% run ../sedindex logics to prepare index file
+
+\makeindex
+\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
+\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
+\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
+\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
+
+\underscoreoff
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
+
+\pagestyle{headings}
+%\sloppy
+%\binperiod %%%treat . like a binary operator
+
+\begin{document}
+\title{\includegraphics[scale=.8]{isabelle_hol}
+ \\ \vspace{0.5cm} The Tutorial
+ \\ --- DRAFT ---}
+\author{Tobias Nipkow\\
+Technische Universit\"at M\"unchen \\
+Institut f\"ur Informatik \\
+\url{http://www.in.tum.de/~nipkow/}}
+\maketitle
+
+\pagenumbering{roman}
+\tableofcontents
+
+\subsubsection*{Acknowledgements}
+This tutorial owes a lot to the constant discussions with and the valuable
+feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
+Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
+and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
+read and comment on a draft version.
+\clearfirst
+
+\input{basics}
+\input{fp}
+\input{appendix}
+
+\bibliographystyle{plain}
+\bibliography{../manual}
+\input{tutorial.ind}
+\end{document}