--- a/doc-src/TutorialI/Misc/Tree.thy Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/Tree.thy Fri Jan 05 18:32:57 2001 +0100
@@ -8,14 +8,14 @@
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
-consts mirror :: "'a tree \\<Rightarrow> 'a tree";
+consts mirror :: "'a tree \<Rightarrow> 'a tree";
primrec
"mirror Tip = Tip"
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
and a function @{term"mirror"} that mirrors a binary tree
-by swapping subtrees (recursively). Prove
+by swapping subtrees recursively. Prove
*}
lemma mirror_mirror: "mirror(mirror t) = t";