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

     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	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 31250	cf75908fd3c3
child 43382	bf89455ccf9d
permissions	-rw-r--r--