Updated function tutorial: Types can be inferred and need not be given anymore

--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri Oct 19 07:48:25 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri Oct 19 09:59:46 2007 +0200
@@ -23,8 +23,12 @@
 
 text {*
   The syntax is rather self-explanatory: We introduce a function by
-  giving its name, its type and a set of defining recursive
-  equations.
+  giving its name, its type, 
+  and a set of defining recursive equations.
+  If we leave out the type, the most general type will be
+  inferred, which can sometimes lead to surprises: Since both @{term
+  "1::nat"} and @{text plus} are overloaded, we would end up
+  with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}.
 *}
 
 text {*

--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Fri Oct 19 07:48:25 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Fri Oct 19 09:59:46 2007 +0200
@@ -36,8 +36,11 @@
 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 The syntax is rather self-explanatory: We introduce a function by
-  giving its name, its type and a set of defining recursive
-  equations.%
+  giving its name, its type, 
+  and a set of defining recursive equations.
+  If we leave out the type, the most general type will be
+  inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{plus} are overloaded, we would end up
+  with \isa{fib\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}one{\isacharcomma}plus{\isacharbraceright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %