# HG changeset patch
# User nipkow
# Date 1323331844 -3600
# Node ID ddac6eb800c699eed2f2eded06f671999dff70eb
# Parent  9b11989f38b0d68de19a24acba69018659a7a7d5
tuned

diff -r 9b11989f38b0 -r ddac6eb800c6 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Dec 07 11:24:45 2011 +0100
+++ b/src/HOL/IMP/Live.thy	Thu Dec 08 09:10:44 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)