1 % pr(latex xsymbols symbols)
2 \documentclass[11pt,a4paper]{report}
3 \usepackage{isabelle,isabellesym}
4 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
5 \usepackage{../pdfsetup} %last package!
7 \newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
9 %\newtheorem{theorem}{Theorem}[section]
10 \newtheorem{Exercise}{Exercise}[section]
11 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
12 \newcommand{\ttlbr}{\texttt{[|}}
13 \newcommand{\ttrbr}{\texttt{|]}}
14 \newcommand{\ttor}{\texttt{|}}
15 \newcommand{\ttall}{\texttt{!}}
16 \newcommand{\ttuniquex}{\texttt{?!}}
17 \newcommand{\ttEXU}{\texttt{EX!}}
18 \newcommand{\ttAnd}{\texttt{!!}}
20 \newcommand{\isasymimp}{\isasymlongrightarrow}
21 \newcommand{\isasymImp}{\isasymLongrightarrow}
22 \newcommand{\isasymFun}{\isasymRightarrow}
23 \newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
25 \newenvironment{isabellepar}%
26 {\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
28 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
30 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
31 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
32 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
33 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
34 %% run ../sedindex logics to prepare index file
37 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
38 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
39 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
40 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
44 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
48 %\binperiod %%%treat . like a binary operator
51 \title{\includegraphics[scale=.8]{isabelle_hol}
52 \\ \vspace{0.5cm} The Tutorial
54 \author{Tobias Nipkow\\
55 Technische Universit\"at M\"unchen \\
56 Institut f\"ur Informatik \\
57 \url{http://www.in.tum.de/~nipkow/}}
63 \subsubsection*{Acknowledgements}
64 This tutorial owes a lot to the constant discussions with and the valuable
65 feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
66 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
67 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
68 read and comment on a draft version.
75 \bibliographystyle{plain}
76 \bibliography{../manual}