# HG changeset patch
# User nipkow
# Date 1323331854 -3600
# Node ID 192243fd94a503df4463f38e980a6dbc4f70d732
# Parent  3e8a2464f6071f1a7b8cc6b28f2859351b49a271# Parent  ddac6eb800c699eed2f2eded06f671999dff70eb
merged

diff -r 3e8a2464f607 -r 192243fd94a5 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Dec 07 16:06:08 2011 +0000
+++ b/src/HOL/IMP/Live.thy	Thu Dec 08 09:10:54 2011 +0100
@@ -39,7 +39,7 @@
 by(auto simp add:L_gen_kill)
 
 lemma L_While_lpfp:
-  "\<lbrakk> vars b \<union> X \<subseteq> P; L c P \<subseteq> P \<rbrakk> \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
+  "vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
 by(simp add: L_gen_kill)