src/HOL/Library/Tree.thy

 "heap Leaf = True" |
 "heap (Node l m r) =
   (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
 
 
-subsection "Function @{text mirror}"
+subsection "Function \<open>mirror\<close>"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror \<langle>\<rangle> = Leaf" |
 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>"