src/HOL/Hoare_Parallel/OG_Tran.thy
changeset 35107 bdca9f765ee4
parent 32960 69916a850301
child 35416 d8d7d1b785af
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Thu Feb 11 09:14:34 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Thu Feb 11 13:54:53 2010 +0100
@@ -69,7 +69,7 @@
 
 monos "rtrancl_mono"
 
-text {* The corresponding syntax translations are: *}
+text {* The corresponding abbreviations are: *}
 
 abbreviation
   ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) 
@@ -101,8 +101,8 @@
   SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set"
   "SEM c S \<equiv> \<Union>sem c ` S "
 
-syntax "_Omega" :: "'a com"    ("\<Omega>" 63)
-translations  "\<Omega>" \<rightleftharpoons> "While CONST UNIV CONST UNIV (Basic id)"
+abbreviation Omega :: "'a com"    ("\<Omega>" 63)
+  where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
 
 consts fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com"
 primrec