src/CCL/Trancl.thy

--- a/src/CCL/Trancl.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Trancl.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -25,7 +25,7 @@
   where "r^+ == r O rtrancl(r)"
 
 
-subsection \<open>Natural deduction for @{text "trans(r)"}\<close>
+subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close>
 
 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)"
   unfolding trans_def by blast