--- a/doc-src/TutorialI/Recdef/examples.thy Tue Feb 20 10:37:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy Tue Feb 20 11:27:04 2001 +0100
@@ -57,8 +57,11 @@
"sep1(a, xs) = xs";
text{*\noindent
-This defines exactly the same function as @{term"sep"} above, i.e.\
-@{prop"sep1 = sep"}.
+To guarantee that the second equation can only be applied if the first
+one does not match, Isabelle internally replaces the second equation
+by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
+@{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and
+@{term sep1} are identical.
\begin{warn}
\isacommand{recdef} only takes the first argument of a (curried)