author | krauss |
Thu, 17 May 2007 23:03:47 +0200 | |
changeset 23003 | 4b0bf04a4d68 |
parent 21212 | 547224bf9348 |
child 23188 | 595a0e24bd8e |
permissions | -rw-r--r-- |
krauss@21212 | 1 |
|
krauss@21212 | 2 |
%% $Id$ |
krauss@21212 | 3 |
|
krauss@23003 | 4 |
\documentclass[11pt,a4paper,fleqn]{article} |
krauss@23003 | 5 |
\textwidth 15.93cm |
krauss@23003 | 6 |
\textheight 24cm |
krauss@23003 | 7 |
\oddsidemargin 0.0cm |
krauss@23003 | 8 |
\evensidemargin 0.0cm |
krauss@23003 | 9 |
\topmargin 0.0cm |
krauss@23003 | 10 |
|
krauss@21212 | 11 |
\usepackage{latexsym,graphicx} |
krauss@21212 | 12 |
\usepackage[refpage]{nomencl} |
krauss@21212 | 13 |
\usepackage{../../iman,../../extra,../../isar,../../proof} |
krauss@21212 | 14 |
\usepackage{Thy/document/isabelle,Thy/document/isabellesym} |
krauss@21212 | 15 |
\usepackage{style} |
krauss@21212 | 16 |
\usepackage{Thy/document/pdfsetup} |
krauss@23003 | 17 |
\usepackage{mathpartir} |
krauss@23003 | 18 |
\usepackage{amsthm} |
krauss@21212 | 19 |
|
krauss@21212 | 20 |
\newcommand{\cmd}[1]{\isacommand{#1}} |
krauss@21212 | 21 |
|
krauss@21212 | 22 |
\newcommand{\isasymINFIX}{\cmd{infix}} |
krauss@21212 | 23 |
\newcommand{\isasymLOCALE}{\cmd{locale}} |
krauss@21212 | 24 |
\newcommand{\isasymINCLUDES}{\cmd{includes}} |
krauss@21212 | 25 |
\newcommand{\isasymDATATYPE}{\cmd{datatype}} |
krauss@21212 | 26 |
\newcommand{\isasymAXCLASS}{\cmd{axclass}} |
krauss@21212 | 27 |
\newcommand{\isasymFIXES}{\cmd{fixes}} |
krauss@21212 | 28 |
\newcommand{\isasymASSUMES}{\cmd{assumes}} |
krauss@21212 | 29 |
\newcommand{\isasymDEFINES}{\cmd{defines}} |
krauss@21212 | 30 |
\newcommand{\isasymNOTES}{\cmd{notes}} |
krauss@21212 | 31 |
\newcommand{\isasymSHOWS}{\cmd{shows}} |
krauss@21212 | 32 |
\newcommand{\isasymCLASS}{\cmd{class}} |
krauss@21212 | 33 |
\newcommand{\isasymINSTANCE}{\cmd{instance}} |
krauss@21212 | 34 |
\newcommand{\isasymLEMMA}{\cmd{lemma}} |
krauss@21212 | 35 |
\newcommand{\isasymPROOF}{\cmd{proof}} |
krauss@21212 | 36 |
\newcommand{\isasymQED}{\cmd{qed}} |
krauss@21212 | 37 |
\newcommand{\isasymFIX}{\cmd{fix}} |
krauss@21212 | 38 |
\newcommand{\isasymASSUME}{\cmd{assume}} |
krauss@21212 | 39 |
\newcommand{\isasymSHOW}{\cmd{show}} |
krauss@21212 | 40 |
\newcommand{\isasymNOTE}{\cmd{note}} |
krauss@21212 | 41 |
\newcommand{\isasymIN}{\cmd{in}} |
krauss@21212 | 42 |
\newcommand{\isasymCODEGEN}{\cmd{code\_gen}} |
krauss@21212 | 43 |
\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}} |
krauss@21212 | 44 |
\newcommand{\isasymFUN}{\cmd{fun}} |
krauss@21212 | 45 |
\newcommand{\isasymFUNCTION}{\cmd{function}} |
krauss@21212 | 46 |
\newcommand{\isasymPRIMREC}{\cmd{primrec}} |
krauss@21212 | 47 |
\newcommand{\isasymRECDEF}{\cmd{recdef}} |
krauss@21212 | 48 |
|
krauss@21212 | 49 |
\newcommand{\qt}[1]{``#1''} |
krauss@21212 | 50 |
\newcommand{\qtt}[1]{"{}{#1}"{}} |
krauss@21212 | 51 |
\newcommand{\qn}[1]{\emph{#1}} |
krauss@21212 | 52 |
\newcommand{\strong}[1]{{\bfseries #1}} |
krauss@21212 | 53 |
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}} |
krauss@21212 | 54 |
|
krauss@23003 | 55 |
\newtheorem{exercise}{Exercise}{\bf}{\itshape} |
krauss@23003 | 56 |
%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape} |
krauss@21212 | 57 |
|
krauss@21212 | 58 |
\hyphenation{Isabelle} |
krauss@21212 | 59 |
\hyphenation{Isar} |
krauss@21212 | 60 |
|
krauss@21212 | 61 |
\isadroptag{theory} |
krauss@23003 | 62 |
\title{Defining Recursive Functions in Isabelle/HOL} |
krauss@23003 | 63 |
\author{Alexander Krauss} |
krauss@21212 | 64 |
|
krauss@21212 | 65 |
|
krauss@21212 | 66 |
\isabellestyle{tt} |
krauss@21212 | 67 |
|
krauss@21212 | 68 |
\begin{document} |
krauss@21212 | 69 |
|
krauss@21212 | 70 |
\maketitle |
krauss@21212 | 71 |
|
krauss@21212 | 72 |
\begin{abstract} |
krauss@21212 | 73 |
This tutorial describes the use of the new \emph{function} package, |
krauss@23003 | 74 |
which provides general recursive function definitions for Isabelle/HOL. |
krauss@23003 | 75 |
|
krauss@23003 | 76 |
|
krauss@23003 | 77 |
% starting with very simple examples and the proceeding to the more |
krauss@23003 | 78 |
% intricate ones. |
krauss@21212 | 79 |
\end{abstract} |
krauss@21212 | 80 |
|
krauss@23003 | 81 |
%\thispagestyle{empty}\clearpage |
krauss@21212 | 82 |
|
krauss@23003 | 83 |
%\pagenumbering{roman} |
krauss@23003 | 84 |
%\clearfirst |
krauss@21212 | 85 |
|
krauss@23003 | 86 |
\input{intro.tex} |
krauss@21212 | 87 |
\input{Thy/document/Functions.tex} |
krauss@21212 | 88 |
|
krauss@21212 | 89 |
\begingroup |
krauss@21212 | 90 |
%\tocentry{\bibname} |
krauss@21212 | 91 |
\bibliographystyle{plain} \small\raggedright\frenchspacing |
krauss@21212 | 92 |
\bibliography{../../manual} |
krauss@21212 | 93 |
\endgroup |
krauss@21212 | 94 |
|
krauss@21212 | 95 |
\end{document} |
krauss@21212 | 96 |
|
krauss@21212 | 97 |
|
krauss@21212 | 98 |
%%% Local Variables: |
krauss@21212 | 99 |
%%% mode: latex |
krauss@21212 | 100 |
%%% TeX-master: t |
krauss@21212 | 101 |
%%% End: |