1
2\documentclass[a4paper,fleqn]{article}
3
4\usepackage{latexsym,graphicx}
5\usepackage[refpage]{nomencl}
6\usepackage{iman,extra,isar}
7\usepackage{isabelle,isabellesym}
8\usepackage{style}
9\usepackage{mathpartir}
10\usepackage{amsthm}
11\usepackage{pdfsetup}
12
13\newcommand{\cmd}[1]{\isacommand{#1}}
14
15\newcommand{\isasymINFIX}{\cmd{infix}}
16\newcommand{\isasymLOCALE}{\cmd{locale}}
17\newcommand{\isasymINCLUDES}{\cmd{includes}}
18\newcommand{\isasymDATATYPE}{\cmd{datatype}}
19\newcommand{\isasymDEFINES}{\cmd{defines}}
20\newcommand{\isasymNOTES}{\cmd{notes}}
21\newcommand{\isasymCLASS}{\cmd{class}}
22\newcommand{\isasymINSTANCE}{\cmd{instance}}
23\newcommand{\isasymLEMMA}{\cmd{lemma}}
24\newcommand{\isasymPROOF}{\cmd{proof}}
25\newcommand{\isasymQED}{\cmd{qed}}
26\newcommand{\isasymFIX}{\cmd{fix}}
27\newcommand{\isasymASSUME}{\cmd{assume}}
28\newcommand{\isasymSHOW}{\cmd{show}}
29\newcommand{\isasymNOTE}{\cmd{note}}
30\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
31\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
32\newcommand{\isasymFUN}{\cmd{fun}}
33\newcommand{\isasymFUNCTION}{\cmd{function}}
34\newcommand{\isasymPRIMREC}{\cmd{primrec}}
35\newcommand{\isasymRECDEF}{\cmd{recdef}}
36
37\newcommand{\qt}[1]{``#1''}
38\newcommand{\qtt}[1]{"{}{#1}"{}}
39\newcommand{\qn}[1]{\emph{#1}}
40\newcommand{\strong}[1]{{\bfseries #1}}
41\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
42
43\newtheorem{exercise}{Exercise}{\bf}{\itshape}
44%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}
45
46\hyphenation{Isabelle}
47\hyphenation{Isar}
48
49\isadroptag{theory}
50\title{Defining Recursive Functions in Isabelle/HOL}
51\author{Alexander Krauss}
52
53\isabellestyle{tt}
54
55\begin{document}
56
57\date{\ \\}
58\maketitle
59
60\begin{abstract}
61  This tutorial describes the use of the \emph{function} package,
62	which provides general recursive function definitions for Isabelle/HOL.
63	We start with very simple examples and then gradually move on to more
64	advanced topics such as manual termination proofs, nested recursion,
65	partiality, tail recursion and congruence rules.
66\end{abstract}
67
68%\thispagestyle{empty}\clearpage
69
70%\pagenumbering{roman}
71%\clearfirst
72
73\input{intro.tex}
74\input{Functions.tex}
75%\input{conclusion.tex}
76
77\begingroup
78%\tocentry{\bibname}
79\bibliographystyle{plain} \small\raggedright\frenchspacing
80\bibliography{manual}
81\endgroup
82
83\end{document}
84
85
86%%% Local Variables: 
87%%% mode: latex
88%%% TeX-master: t
89%%% End: 
90