1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/tutorial.tex	Wed Apr 19 11:54:39 2000 +0200
     1.3 @@ -0,0 +1,78 @@
     1.4 +\documentclass[11pt,a4paper]{report}
     1.5 +\usepackage{isabelle,isabellesym,pdfsetup}
     1.6 +\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
     1.7 +
     1.8 +\usepackage{ttbox}
     1.9 +\newcommand\ttbreak{\vskip-10pt\pagebreak[0]}
    1.10 +\newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
    1.11 +
    1.12 +%\newtheorem{theorem}{Theorem}[section]
    1.13 +\newtheorem{Exercise}{Exercise}[section]
    1.14 +\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
    1.15 +\newcommand{\ttlbr}{\texttt{[|}}
    1.16 +\newcommand{\ttrbr}{\texttt{|]}}
    1.17 +\newcommand{\ttor}{\texttt{|}}
    1.18 +\newcommand{\ttall}{\texttt{!}}
    1.19 +\newcommand{\ttuniquex}{\texttt{?!}}
    1.20 +\newcommand{\ttEXU}{\texttt{EX!}}
    1.21 +\newcommand{\ttAnd}{\texttt{!!}}
    1.22 +
    1.23 +\newcommand{\isasymimp}{\isasymlongrightarrow}
    1.24 +\newcommand{\isasymImp}{\isasymLongrightarrow}
    1.25 +\newcommand{\isasymFun}{\isasymRightarrow}
    1.26 +\newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
    1.27 +
    1.28 +\newenvironment{isabellepar}%
    1.29 +{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
    1.30 +
    1.31 +\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
    1.32 +
    1.33 +%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.34 +%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.35 +%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.36 +%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    1.37 +%% run    ../sedindex logics    to prepare index file
    1.38 +
    1.39 +\makeindex
    1.40 +\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
    1.41 +\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
    1.42 +\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
    1.43 +\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
    1.44 +
    1.45 +\underscoreoff
    1.46 +
    1.47 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.48 +
    1.49 +\pagestyle{headings}
    1.50 +%\sloppy
    1.51 +%\binperiod     %%%treat . like a binary operator
    1.52 +
    1.53 +\begin{document}
    1.54 +\title{\includegraphics[scale=.8]{isabelle_hol}
    1.55 +       \\ \vspace{0.5cm} The Tutorial
    1.56 +       \\ --- DRAFT ---}
    1.57 +\author{Tobias Nipkow\\
    1.58 +Technische Universit\"at M\"unchen \\
    1.59 +Institut f\"ur Informatik \\
    1.60 +\url{http://www.in.tum.de/~nipkow/}}
    1.61 +\maketitle
    1.62 +
    1.63 +\pagenumbering{roman}
    1.64 +\tableofcontents
    1.65 +
    1.66 +\subsubsection*{Acknowledgements}
    1.67 +This tutorial owes a lot to the constant discussions with and the valuable
    1.68 +feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
    1.69 +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
    1.70 +and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
    1.71 +read and comment on a draft version.
    1.72 +\clearfirst
    1.73 +
    1.74 +\input{basics}
    1.75 +\input{fp}
    1.76 +\input{appendix}
    1.77 +
    1.78 +\bibliographystyle{plain}
    1.79 +\bibliography{../manual}
    1.80 +\input{tutorial.ind}
    1.81 +\end{document}