diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Misc/Tree.thy
--- a/doc-src/TutorialI/Misc/Tree.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -14,7 +14,7 @@
 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
 
 text{*\noindent
-and a function \isa{mirror} that mirrors a binary tree
+and a function @{term"mirror"} that mirrors a binary tree
 by swapping subtrees (recursively). Prove
 *}
 
@@ -30,7 +30,7 @@
 (*>*)
 
 text{*\noindent
-Define a function \isa{flatten} that flattens a tree into a list
+Define a function @{term"flatten"} that flattens a tree into a list
 by traversing it in infix order. Prove
 *}