--- a/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 19:17:01 2001 +0200
@@ -62,9 +62,9 @@
*}
consts divi :: "nat \<times> nat \<Rightarrow> nat"
-recdef divi "measure(\<lambda>(m,n). m)"
+recdef (permissive) divi "measure(\<lambda>(m,n). m)"
"divi(m,n) = (if n = 0 then arbitrary else
- if m < n then 0 else divi(m-n,n)+1)"
+ if m < n then 0 else divi(m-n,n)+1)" (* FIXME permissive!? *)
text{*\noindent Of course we could also have defined
@{term"divi(m,0)"} to be some specific number, for example 0. The