# HG changeset patch
# User nipkow
# Date 1404398535 -7200
# Node ID 2cfefeee7bba33dcfda2db7e02e187bdcd07541a
# Parent  b69a1272cb046a33d1615b160ae1f4fc9c21d718
Tail recursion no longer supported by "function".

diff -r b69a1272cb04 -r 2cfefeee7bba src/Doc/Functions/document/intro.tex
--- a/src/Doc/Functions/document/intro.tex	Thu Jul 03 14:40:36 2014 +0200
+++ b/src/Doc/Functions/document/intro.tex	Thu Jul 03 16:42:15 2014 +0200
@@ -50,6 +50,8 @@
 a few of technical issues around \cmd{recdef}, and allow definitions
 which were not previously possible.
 
+In addition there is also the \cmd{partial\_function} command
+(see \cite{isabelle-isar-ref}) that supports the definition of partial
+and tail recursive functions.
 
 
-