src/HOL/Hoare_Parallel/OG_Syntax.thy

--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Jan 02 18:48:45 2016 +0100
@@ -3,7 +3,7 @@
 begin
 
 text\<open>Syntax for commands and for assertions and boolean expressions in
- commands @{text com} and annotated commands @{text ann_com}.\<close>
+ commands \<open>com\<close> and annotated commands \<open>ann_com\<close>.\<close>
 
 abbreviation Skip :: "'a com"  ("SKIP" 63)
   where "SKIP \<equiv> Basic id"