doc-src/Functions/functions.tex
author wenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511 bf89455ccf9d
parent 31256 cf75908fd3c3
permissions -rw-r--r--
eliminated copies of isabelle style files;
     1 
     2 \documentclass[a4paper,fleqn]{article}
     3 
     4 \usepackage{latexsym,graphicx}
     5 \usepackage[refpage]{nomencl}
     6 \usepackage{../iman,../extra,../isar,../proof}
     7 \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     8 \usepackage{style}
     9 \usepackage{mathpartir}
    10 \usepackage{amsthm}
    11 \usepackage{../pdfsetup}
    12 
    13 \newcommand{\cmd}[1]{\isacommand{#1}}
    14 
    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}}
    36 
    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}}
    42 
    43 \newtheorem{exercise}{Exercise}{\bf}{\itshape}
    44 %\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}
    45 
    46 \hyphenation{Isabelle}
    47 \hyphenation{Isar}
    48 
    49 \isadroptag{theory}
    50 \title{Defining Recursive Functions in Isabelle/HOL}
    51 \author{Alexander Krauss}
    52 
    53 \isabellestyle{tt}
    54 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
    55 
    56 \begin{document}
    57 
    58 \date{\ \\}
    59 \maketitle
    60 
    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}
    68 
    69 %\thispagestyle{empty}\clearpage
    70 
    71 %\pagenumbering{roman}
    72 %\clearfirst
    73 
    74 \input{intro.tex}
    75 \input{Thy/document/Functions.tex}
    76 %\input{conclusion.tex}
    77 
    78 \begingroup
    79 %\tocentry{\bibname}
    80 \bibliographystyle{plain} \small\raggedright\frenchspacing
    81 \bibliography{../manual}
    82 \endgroup
    83 
    84 \end{document}
    85 
    86 
    87 %%% Local Variables: 
    88 %%% mode: latex
    89 %%% TeX-master: t
    90 %%% End: