doc-src/TutorialI/tutorial.tex
author nipkow
Wed Apr 19 11:54:39 2000 +0200 (2000-04-19)
changeset 8743 3253c6046d57
child 8828 5be2d1745c61
permissions -rw-r--r--
I wonder if that's all?
nipkow@8743
     1
\documentclass[11pt,a4paper]{report}
nipkow@8743
     2
\usepackage{isabelle,isabellesym,pdfsetup}
nipkow@8743
     3
\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
nipkow@8743
     4
nipkow@8743
     5
\usepackage{ttbox}
nipkow@8743
     6
\newcommand\ttbreak{\vskip-10pt\pagebreak[0]}
nipkow@8743
     7
\newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
nipkow@8743
     8
nipkow@8743
     9
%\newtheorem{theorem}{Theorem}[section]
nipkow@8743
    10
\newtheorem{Exercise}{Exercise}[section]
nipkow@8743
    11
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
nipkow@8743
    12
\newcommand{\ttlbr}{\texttt{[|}}
nipkow@8743
    13
\newcommand{\ttrbr}{\texttt{|]}}
nipkow@8743
    14
\newcommand{\ttor}{\texttt{|}}
nipkow@8743
    15
\newcommand{\ttall}{\texttt{!}}
nipkow@8743
    16
\newcommand{\ttuniquex}{\texttt{?!}}
nipkow@8743
    17
\newcommand{\ttEXU}{\texttt{EX!}}
nipkow@8743
    18
\newcommand{\ttAnd}{\texttt{!!}}
nipkow@8743
    19
nipkow@8743
    20
\newcommand{\isasymimp}{\isasymlongrightarrow}
nipkow@8743
    21
\newcommand{\isasymImp}{\isasymLongrightarrow}
nipkow@8743
    22
\newcommand{\isasymFun}{\isasymRightarrow}
nipkow@8743
    23
\newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
nipkow@8743
    24
nipkow@8743
    25
\newenvironment{isabellepar}%
nipkow@8743
    26
{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
nipkow@8743
    27
nipkow@8743
    28
\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
nipkow@8743
    29
nipkow@8743
    30
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
nipkow@8743
    31
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
nipkow@8743
    32
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
nipkow@8743
    33
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
nipkow@8743
    34
%% run    ../sedindex logics    to prepare index file
nipkow@8743
    35
nipkow@8743
    36
\makeindex
nipkow@8743
    37
\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
nipkow@8743
    38
\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
nipkow@8743
    39
\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
nipkow@8743
    40
\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
nipkow@8743
    41
nipkow@8743
    42
\underscoreoff
nipkow@8743
    43
nipkow@8743
    44
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
nipkow@8743
    45
nipkow@8743
    46
\pagestyle{headings}
nipkow@8743
    47
%\sloppy
nipkow@8743
    48
%\binperiod     %%%treat . like a binary operator
nipkow@8743
    49
nipkow@8743
    50
\begin{document}
nipkow@8743
    51
\title{\includegraphics[scale=.8]{isabelle_hol}
nipkow@8743
    52
       \\ \vspace{0.5cm} The Tutorial
nipkow@8743
    53
       \\ --- DRAFT ---}
nipkow@8743
    54
\author{Tobias Nipkow\\
nipkow@8743
    55
Technische Universit\"at M\"unchen \\
nipkow@8743
    56
Institut f\"ur Informatik \\
nipkow@8743
    57
\url{http://www.in.tum.de/~nipkow/}}
nipkow@8743
    58
\maketitle
nipkow@8743
    59
nipkow@8743
    60
\pagenumbering{roman}
nipkow@8743
    61
\tableofcontents
nipkow@8743
    62
nipkow@8743
    63
\subsubsection*{Acknowledgements}
nipkow@8743
    64
This tutorial owes a lot to the constant discussions with and the valuable
nipkow@8743
    65
feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
nipkow@8743
    66
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
nipkow@8743
    67
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
nipkow@8743
    68
read and comment on a draft version.
nipkow@8743
    69
\clearfirst
nipkow@8743
    70
nipkow@8743
    71
\input{basics}
nipkow@8743
    72
\input{fp}
nipkow@8743
    73
\input{appendix}
nipkow@8743
    74
nipkow@8743
    75
\bibliographystyle{plain}
nipkow@8743
    76
\bibliography{../manual}
nipkow@8743
    77
\input{tutorial.ind}
nipkow@8743
    78
\end{document}