--- a/doc-src/IsarAdvanced/Functions/intro.tex Fri Jun 01 15:18:31 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/intro.tex Fri Jun 01 15:20:53 2007 +0200
@@ -1,11 +1,13 @@
\section{Introduction}
-In Isabelle 2007, new facilities for recursive function definitions
-are available.
+In the upcomung release of Isabelle 2007, new facilities for recursive
+function definitions \cite{krauss2006} will be available.
-This document is intended as a tutorial for both inexperienced and
-advanced users, and demonstrates the use of the package with a lot of
-examples.
+This tutorial is an example-guided introduction to the practical use
+of the package. We assume that you have mastered the basic concepts of
+Isabelle/HOL and are able to write basic specifications and
+proofs. To start out with Isabelle in general, you should read the
+tutorial \cite{isa-tutorial}.
% Definitional extension
@@ -23,9 +25,10 @@
The new \cmd{function} command, and its short form \cmd{fun} will
-replace the traditional \cmd{recdef} command in the future. It solves
+replace the traditional \cmd{recdef} command \cite{slind-tfl} in the future. It solves
a few of technical issues around \cmd{recdef}, and allows definitions
which were not previously possible.
+