src/HOL/UNITY/Lift_prog.thy

--- a/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -178,7 +178,7 @@
 lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
 by (simp add: lift_def)
 
-lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
+lemma lift_Join [simp]: "lift i (F \<squnion> G) = lift i F \<squnion> lift i G"
 by (simp add: lift_def)
 
 lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"