wneuper/isa: doc-src/Functions/functions.tex@cf75908fd3c3

     2 \documentclass[a4paper,fleqn]{article}

     4 \usepackage{latexsym,graphicx}

     5 \usepackage[refpage]{nomencl}

     6 \usepackage{../iman,../extra,../isar,../proof}

     7 \usepackage{../isabelle,../isabellesym}

     8 \usepackage{style}

     9 \usepackage{mathpartir}

    10 \usepackage{amsthm}

    11 \usepackage{../pdfsetup}

    13 \newcommand{\cmd}[1]{\isacommand{#1}}

    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}}

    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}}

    43 \newtheorem{exercise}{Exercise}{\bf}{\itshape}

    44 %\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}

    46 \hyphenation{Isabelle}

    47 \hyphenation{Isar}

    49 \isadroptag{theory}

    50 \title{Defining Recursive Functions in Isabelle/HOL}

    51 \author{Alexander Krauss}

    53 \isabellestyle{tt}

    54 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text

    56 \begin{document}

    58 \date{\ \\}

    59 \maketitle

    61 \begin{abstract}

    62   This tutorial describes the use of the new \emph{function} package,

    63 	which provides general recursive function definitions for Isabelle/HOL.

    64 	We start with very simple examples and then gradually move on to more

    65 	advanced topics such as manual termination proofs, nested recursion,

    66 	partiality, tail recursion and congruence rules.

    67 \end{abstract}

    69 %\thispagestyle{empty}\clearpage

    71 %\pagenumbering{roman}

    72 %\clearfirst

    74 \input{intro.tex}

    75 \input{Thy/document/Functions.tex}

    76 %\input{conclusion.tex}

    78 \begingroup

    79 %\tocentry{\bibname}

    80 \bibliographystyle{plain} \small\raggedright\frenchspacing

    81 \bibliography{../manual}

    82 \endgroup

    84 \end{document}

    87 %%% Local Variables:

    88 %%% mode: latex

    89 %%% TeX-master: t

    90 %%% End:

author	haftmann
	Tue, 26 May 2009 13:40:50 +0200
changeset 31250	cf75908fd3c3
parent 30209	2f4684e2ea95
child 43382	bf89455ccf9d
permissions	-rw-r--r--