equal
deleted
inserted
replaced
60 |
60 |
61 \isadroptag{theory} |
61 \isadroptag{theory} |
62 \title{Defining Recursive Functions in Isabelle/HOL} |
62 \title{Defining Recursive Functions in Isabelle/HOL} |
63 \author{Alexander Krauss} |
63 \author{Alexander Krauss} |
64 |
64 |
65 |
|
66 \isabellestyle{tt} |
65 \isabellestyle{tt} |
|
66 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
67 |
67 |
68 \begin{document} |
68 \begin{document} |
69 |
69 |
70 \maketitle |
70 \maketitle |
71 |
71 |
72 \begin{abstract} |
72 \begin{abstract} |
73 This tutorial describes the use of the new \emph{function} package, |
73 This tutorial describes the use of the new \emph{function} package, |
74 which provides general recursive function definitions for Isabelle/HOL. |
74 which provides general recursive function definitions for Isabelle/HOL. |
75 |
75 We start with very simple examples and then gradually move on to more |
76 |
76 advanced topics such as manual termination proofs, nested recursion, |
77 % starting with very simple examples and the proceeding to the more |
77 partiality and congruence rules. |
78 % intricate ones. |
|
79 \end{abstract} |
78 \end{abstract} |
80 |
79 |
81 %\thispagestyle{empty}\clearpage |
80 %\thispagestyle{empty}\clearpage |
82 |
81 |
83 %\pagenumbering{roman} |
82 %\pagenumbering{roman} |
84 %\clearfirst |
83 %\clearfirst |
85 |
84 |
86 \input{intro.tex} |
85 \input{intro.tex} |
87 \input{Thy/document/Functions.tex} |
86 \input{Thy/document/Functions.tex} |
|
87 \input{conclusion.tex} |
88 |
88 |
89 \begingroup |
89 \begingroup |
90 %\tocentry{\bibname} |
90 %\tocentry{\bibname} |
91 \bibliographystyle{plain} \small\raggedright\frenchspacing |
91 \bibliographystyle{plain} \small\raggedright\frenchspacing |
92 \bibliography{../../manual} |
92 \bibliography{../../manual} |