--- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Feb 20 10:37:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Feb 20 11:27:04 2001 +0100
@@ -52,8 +52,11 @@
\ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-This defines exactly the same function as \isa{sep} above, i.e.\
-\isa{sep{\isadigit{1}}\ {\isacharequal}\ 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: \isa{sep{\isadigit{1}}\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} and
+\isa{sep{\isadigit{1}}\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}}. Thus the functions \isa{sep} and
+\isa{sep{\isadigit{1}}} are identical.
\begin{warn}
\isacommand{recdef} only takes the first argument of a (curried)
--- 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)
--- a/doc-src/TutorialI/todo.tobias Tue Feb 20 10:37:12 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Tue Feb 20 11:27:04 2001 +0100
@@ -3,6 +3,22 @@
- (#2 * x) = #2 * - x is not proved by arith
+a simp command for terms
+
+----------------------------------------------------------------------
+primrec
+"(foorec [] []) = []"
+"(foorec [] (y # ys)) = (y # (foorec [] ys))"
+
+*** Primrec definition error:
+*** extra variables on rhs: "y", "ys"
+*** in
+*** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
+*** At command "primrec".
+
+Bessere Fehlermeldung!
+----------------------------------------------------------------------
+
Relation: comp -> composition
Add map_cong?? (upto 10% slower)
@@ -37,6 +53,12 @@
Minor fixes in the tutorial
===========================
+recdef: failed tcs no longer shown!
+
+Advanced recdef: explain recdef_tc?
+
+say something about definitional approach. In recdef section? At the end?
+
I guess we should say "HOL" everywhere, with a remark early on about the
differences between our HOL and the other one.