1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Functions/functions.tex	Tue Nov 07 12:20:11 2006 +0100
     1.3 @@ -0,0 +1,93 @@
     1.4 +
     1.5 +%% $Id$
     1.6 +
     1.7 +\documentclass[12pt,a4paper,fleqn]{report}
     1.8 +\usepackage{latexsym,graphicx}
     1.9 +\usepackage{listings}
    1.10 +\usepackage[refpage]{nomencl}
    1.11 +\usepackage{../../iman,../../extra,../../isar,../../proof}
    1.12 +\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
    1.13 +\usepackage{style}
    1.14 +\usepackage{Thy/document/pdfsetup}
    1.15 +
    1.16 +\newcommand{\cmd}[1]{\isacommand{#1}}
    1.17 +
    1.18 +\newcommand{\isasymINFIX}{\cmd{infix}}
    1.19 +\newcommand{\isasymLOCALE}{\cmd{locale}}
    1.20 +\newcommand{\isasymINCLUDES}{\cmd{includes}}
    1.21 +\newcommand{\isasymDATATYPE}{\cmd{datatype}}
    1.22 +\newcommand{\isasymAXCLASS}{\cmd{axclass}}
    1.23 +\newcommand{\isasymFIXES}{\cmd{fixes}}
    1.24 +\newcommand{\isasymASSUMES}{\cmd{assumes}}
    1.25 +\newcommand{\isasymDEFINES}{\cmd{defines}}
    1.26 +\newcommand{\isasymNOTES}{\cmd{notes}}
    1.27 +\newcommand{\isasymSHOWS}{\cmd{shows}}
    1.28 +\newcommand{\isasymCLASS}{\cmd{class}}
    1.29 +\newcommand{\isasymINSTANCE}{\cmd{instance}}
    1.30 +\newcommand{\isasymLEMMA}{\cmd{lemma}}
    1.31 +\newcommand{\isasymPROOF}{\cmd{proof}}
    1.32 +\newcommand{\isasymQED}{\cmd{qed}}
    1.33 +\newcommand{\isasymFIX}{\cmd{fix}}
    1.34 +\newcommand{\isasymASSUME}{\cmd{assume}}
    1.35 +\newcommand{\isasymSHOW}{\cmd{show}}
    1.36 +\newcommand{\isasymNOTE}{\cmd{note}}
    1.37 +\newcommand{\isasymIN}{\cmd{in}}
    1.38 +\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
    1.39 +\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
    1.40 +\newcommand{\isasymFUN}{\cmd{fun}}
    1.41 +\newcommand{\isasymFUNCTION}{\cmd{function}}
    1.42 +\newcommand{\isasymPRIMREC}{\cmd{primrec}}
    1.43 +\newcommand{\isasymRECDEF}{\cmd{recdef}}
    1.44 +
    1.45 +\newcommand{\qt}[1]{``#1''}
    1.46 +\newcommand{\qtt}[1]{"{}{#1}"{}}
    1.47 +\newcommand{\qn}[1]{\emph{#1}}
    1.48 +\newcommand{\strong}[1]{{\bfseries #1}}
    1.49 +\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
    1.50 +
    1.51 +\lstset{basicstyle=\scriptsize\ttfamily, keywordstyle=\itshape, commentstyle=\itshape\sffamily, frame=shadowbox}
    1.52 +\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
    1.53 +\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
    1.54 +
    1.55 +\hyphenation{Isabelle}
    1.56 +\hyphenation{Isar}
    1.57 +
    1.58 +\isadroptag{theory}
    1.59 +\title{\includegraphics[scale=0.5]{isabelle_isar}
    1.60 +  \\[4ex] Defining Recursive Functions in Isabelle/HOL}
    1.61 +\author{\emph{Alexander Krauss}}
    1.62 +
    1.63 +
    1.64 +\isabellestyle{tt}
    1.65 +
    1.66 +\begin{document}
    1.67 +
    1.68 +\maketitle
    1.69 +
    1.70 +\begin{abstract}
    1.71 +  This tutorial describes the use of the new \emph{function} package,
    1.72 +  starting with very simple examples and the proceeding to the more
    1.73 +  intricate ones. No familiarity with other definition facilities is
    1.74 +  assumed.
    1.75 +\end{abstract}
    1.76 +
    1.77 +\thispagestyle{empty}\clearpage
    1.78 +
    1.79 +\pagenumbering{roman}
    1.80 +\clearfirst
    1.81 +
    1.82 +\input{Thy/document/Functions.tex}
    1.83 +
    1.84 +\begingroup
    1.85 +%\tocentry{\bibname}
    1.86 +\bibliographystyle{plain} \small\raggedright\frenchspacing
    1.87 +\bibliography{../../manual}
    1.88 +\endgroup
    1.89 +
    1.90 +\end{document}
    1.91 +
    1.92 +
    1.93 +%%% Local Variables: 
    1.94 +%%% mode: latex
    1.95 +%%% TeX-master: t
    1.96 +%%% End: