--- a/doc-src/TutorialI/Misc/Tree.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Thu Jul 26 16:43:02 2001 +0200
@@ -3,7 +3,7 @@
(*>*)
text{*\noindent
-Define the datatype of binary trees
+Define the datatype of \rmindex{binary trees}:
*}
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
@@ -14,7 +14,7 @@
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
-and a function @{term"mirror"} that mirrors a binary tree
+Define a function @{term"mirror"} that mirrors a binary tree
by swapping subtrees recursively. Prove
*}