--- 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.