doc-src/IsarAdvanced/Functions/intro.tex
changeset 26851 0242c9c980df
parent 23805 953eb3c5f793
child 27026 3602b81665b5
equal deleted inserted replaced
26850:d889d57445dc 26851:0242c9c980df
     1 \section{Introduction}
     1 \section{Introduction}
     2 
     2 
     3 In the upcoming release of Isabelle 2007, new facilities for recursive
     3 Since the release of Isabelle 2007, new facilities for recursive
     4 function definitions \cite{krauss2006} will be available, providing
     4 function definitions~\cite{krauss2006} are available. They provide
     5 better support for general recursive definitions than previous
     5 better support for general recursive definitions than previous
     6 packages did.  But despite all tool support, function definitions can
     6 packages.  But despite all tool support, function definitions can
     7 sometimes be a difficult thing. 
     7 sometimes be a difficult thing. 
     8 
     8 
     9 This tutorial is an example-guided introduction to the practical use
     9 This tutorial is an example-guided introduction to the practical use
    10 of the package and related tools. It should help you get started with
    10 of the package and related tools. It should help you get started with
    11 defining functions quickly. For the more difficult definitions we will
    11 defining functions quickly. For the more difficult definitions we will