src/ZF/Order.thy

--- a/src/ZF/Order.thy	Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Order.thy	Mon Dec 07 10:23:50 2015 +0100
@@ -11,8 +11,8 @@
 
 theory Order imports WF Perm begin
 
-text \<open>We adopt the following convention: @{text ord} is used for
-  strict orders and @{text order} is used for their reflexive
+text \<open>We adopt the following convention: \<open>ord\<close> is used for
+  strict orders and \<open>order\<close> is used for their reflexive
   counterparts.\<close>
 
 definition