wneuper/isa: doc-src/IsarAdvanced/Functions/functions.tex@3197b895f858

     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{\isasymAXCLASS}{\cmd{axclass}}

    20 \newcommand{\isasymDEFINES}{\cmd{defines}}

    21 \newcommand{\isasymNOTES}{\cmd{notes}}

    22 \newcommand{\isasymCLASS}{\cmd{class}}

    23 \newcommand{\isasymINSTANCE}{\cmd{instance}}

    24 \newcommand{\isasymLEMMA}{\cmd{lemma}}

    25 \newcommand{\isasymPROOF}{\cmd{proof}}

    26 \newcommand{\isasymQED}{\cmd{qed}}

    27 \newcommand{\isasymFIX}{\cmd{fix}}

    28 \newcommand{\isasymASSUME}{\cmd{assume}}

    29 \newcommand{\isasymSHOW}{\cmd{show}}

    30 \newcommand{\isasymNOTE}{\cmd{note}}

    31 \newcommand{\isasymCODEGEN}{\cmd{code\_gen}}

    32 \newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}

    33 \newcommand{\isasymFUN}{\cmd{fun}}

    34 \newcommand{\isasymFUNCTION}{\cmd{function}}

    35 \newcommand{\isasymPRIMREC}{\cmd{primrec}}

    36 \newcommand{\isasymRECDEF}{\cmd{recdef}}

    38 \newcommand{\qt}[1]{``#1''}

    39 \newcommand{\qtt}[1]{"{}{#1}"{}}

    40 \newcommand{\qn}[1]{\emph{#1}}

    41 \newcommand{\strong}[1]{{\bfseries #1}}

    42 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}}

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

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

    47 \hyphenation{Isabelle}

    48 \hyphenation{Isar}

    50 \isadroptag{theory}

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

    52 \author{Alexander Krauss}

    54 \isabellestyle{tt}

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

    57 \begin{document}

    59 \date{\ \\}

    60 \maketitle

    62 \begin{abstract}

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

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

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

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

    67 	partiality, tail recursion and congruence rules.

    68 \end{abstract}

    70 %\thispagestyle{empty}\clearpage

    72 %\pagenumbering{roman}

    73 %\clearfirst

    75 \input{intro.tex}

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

    77 %\input{conclusion.tex}

    79 \begingroup

    80 %\tocentry{\bibname}

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

    82 \bibliography{../../manual}

    83 \endgroup

    85 \end{document}

    88 %%% Local Variables:

    89 %%% mode: latex

    90 %%% TeX-master: t

    91 %%% End:

author	wenzelm
	Mon, 16 Feb 2009 12:57:53 +0100
changeset 30076	3197b895f858
parent 26911	871cc7f11034
permissions	-rw-r--r--