1 |
1 |
2 %% $Id$ |
2 %% $Id$ |
3 |
3 |
4 \documentclass[12pt,a4paper,fleqn]{report} |
4 \documentclass[11pt,a4paper,fleqn]{article} |
|
5 \textwidth 15.93cm |
|
6 \textheight 24cm |
|
7 \oddsidemargin 0.0cm |
|
8 \evensidemargin 0.0cm |
|
9 \topmargin 0.0cm |
|
10 |
5 \usepackage{latexsym,graphicx} |
11 \usepackage{latexsym,graphicx} |
6 \usepackage{listings} |
|
7 \usepackage[refpage]{nomencl} |
12 \usepackage[refpage]{nomencl} |
8 \usepackage{../../iman,../../extra,../../isar,../../proof} |
13 \usepackage{../../iman,../../extra,../../isar,../../proof} |
9 \usepackage{Thy/document/isabelle,Thy/document/isabellesym} |
14 \usepackage{Thy/document/isabelle,Thy/document/isabellesym} |
10 \usepackage{style} |
15 \usepackage{style} |
11 \usepackage{Thy/document/pdfsetup} |
16 \usepackage{Thy/document/pdfsetup} |
|
17 \usepackage{mathpartir} |
|
18 \usepackage{amsthm} |
12 |
19 |
13 \newcommand{\cmd}[1]{\isacommand{#1}} |
20 \newcommand{\cmd}[1]{\isacommand{#1}} |
14 |
21 |
15 \newcommand{\isasymINFIX}{\cmd{infix}} |
22 \newcommand{\isasymINFIX}{\cmd{infix}} |
16 \newcommand{\isasymLOCALE}{\cmd{locale}} |
23 \newcommand{\isasymLOCALE}{\cmd{locale}} |
43 \newcommand{\qtt}[1]{"{}{#1}"{}} |
50 \newcommand{\qtt}[1]{"{}{#1}"{}} |
44 \newcommand{\qn}[1]{\emph{#1}} |
51 \newcommand{\qn}[1]{\emph{#1}} |
45 \newcommand{\strong}[1]{{\bfseries #1}} |
52 \newcommand{\strong}[1]{{\bfseries #1}} |
46 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}} |
53 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}} |
47 |
54 |
48 \lstset{basicstyle=\scriptsize\ttfamily, keywordstyle=\itshape, commentstyle=\itshape\sffamily, frame=shadowbox} |
55 \newtheorem{exercise}{Exercise}{\bf}{\itshape} |
49 \newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}} |
56 %\newtheorem*{thmstar}{Theorem}{\bf}{\itshape} |
50 \newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}} |
|
51 |
57 |
52 \hyphenation{Isabelle} |
58 \hyphenation{Isabelle} |
53 \hyphenation{Isar} |
59 \hyphenation{Isar} |
54 |
60 |
55 \isadroptag{theory} |
61 \isadroptag{theory} |
56 \title{\includegraphics[scale=0.5]{isabelle_isar} |
62 \title{Defining Recursive Functions in Isabelle/HOL} |
57 \\[4ex] Defining Recursive Functions in Isabelle/HOL} |
63 \author{Alexander Krauss} |
58 \author{\emph{Alexander Krauss}} |
|
59 |
64 |
60 |
65 |
61 \isabellestyle{tt} |
66 \isabellestyle{tt} |
62 |
67 |
63 \begin{document} |
68 \begin{document} |
64 |
69 |
65 \maketitle |
70 \maketitle |
66 |
71 |
67 \begin{abstract} |
72 \begin{abstract} |
68 This tutorial describes the use of the new \emph{function} package, |
73 This tutorial describes the use of the new \emph{function} package, |
69 starting with very simple examples and the proceeding to the more |
74 which provides general recursive function definitions for Isabelle/HOL. |
70 intricate ones. No familiarity with other definition facilities is |
75 |
71 assumed. |
76 |
|
77 % starting with very simple examples and the proceeding to the more |
|
78 % intricate ones. |
72 \end{abstract} |
79 \end{abstract} |
73 |
80 |
74 \thispagestyle{empty}\clearpage |
81 %\thispagestyle{empty}\clearpage |
75 |
82 |
76 \pagenumbering{roman} |
83 %\pagenumbering{roman} |
77 \clearfirst |
84 %\clearfirst |
78 |
85 |
|
86 \input{intro.tex} |
79 \input{Thy/document/Functions.tex} |
87 \input{Thy/document/Functions.tex} |
80 |
88 |
81 \begingroup |
89 \begingroup |
82 %\tocentry{\bibname} |
90 %\tocentry{\bibname} |
83 \bibliographystyle{plain} \small\raggedright\frenchspacing |
91 \bibliographystyle{plain} \small\raggedright\frenchspacing |