src/Doc/Tutorial/Misc/Tree.thy

 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror Tip = Tip" |
 "mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
 
 text\<open>\noindent
-Define a function @{term"mirror"} that mirrors a binary tree
+Define a function \<^term>\<open>mirror\<close> that mirrors a binary tree
 by swapping subtrees recursively. Prove
 \<close>
 
 lemma mirror_mirror: "mirror(mirror t) = t"
 (*<*)

 "flatten Tip = []" |
 "flatten (Node l x r) = flatten l @ [x] @ flatten r"
 (*>*)
 
 text\<open>\noindent
-Define a function @{term"flatten"} that flattens a tree into a list
+Define a function \<^term>\<open>flatten\<close> that flattens a tree into a list
 by traversing it in infix order. Prove
 \<close>
 
 lemma "flatten(mirror t) = rev(flatten t)"
 (*<*)