src/HOL/Hoare_Parallel/RG_Tran.thy

   ctran :: "('a conf \<times> 'a conf) set"
   and ctran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c\<rightarrow> _" [81,81] 80)
   and ctrans :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c*\<rightarrow> _" [81,81] 80)
 where
   "P -c\<rightarrow> Q \<equiv> (P,Q) \<in> ctran"
-| "P -c*\<rightarrow> Q \<equiv> (P,Q) \<in> ctran^*"
+| "P -c*\<rightarrow> Q \<equiv> (P,Q) \<in> ctran\<^sup>*"
 
 | Basic:  "(Some(Basic f), s) -c\<rightarrow> (None, f s)"
 
 | Seq1:   "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)"