doc-src/TutorialI/tutorial.tex
 author nipkow Tue, 17 Oct 2000 13:28:57 +0200 changeset 10236 7626cb4e1407 parent 10212 33fe2d701ddd child 10272 c02171c5fb20 permissions -rw-r--r--
*** empty log message ***

% pr(latex xsymbols symbols)
\documentclass[11pt,a4paper]{report}
\usepackage{isabelle,isabellesym}
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
\usepackage{../pdfsetup}    %last package!

%\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!\,$}}

\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}???

%\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{\"a}t M{\"u}nchen \\
Institut f{\"u}r 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{\"u}ller,
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}
\chapter{The Rules of the Game}
\label{ch:Rules}
\input{sets}
\input{Inductive/inductive}