--- a/doc-src/TutorialI/Misc/Tree.thy Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Thu May 29 22:45:33 2008 +0200
@@ -8,9 +8,8 @@
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
-consts mirror :: "'a tree \<Rightarrow> 'a tree";
-primrec
-"mirror Tip = Tip"
+primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
+"mirror Tip = Tip" |
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
@@ -23,9 +22,8 @@
apply(induct_tac t);
by(auto);
-consts flatten :: "'a tree => 'a list"
-primrec
-"flatten Tip = []"
+primrec flatten :: "'a tree => 'a list" where
+"flatten Tip = []" |
"flatten (Node l x r) = flatten l @ [x] @ flatten r";
(*>*)