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

     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	haftmann
	Tue, 03 Mar 2009 11:00:51 +0100
changeset 30209	2f4684e2ea95
parent 30076	doc-src/IsarAdvanced/Functions/functions.tex@3197b895f858
child 31250	cf75908fd3c3
permissions	-rw-r--r--