Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Thu, 08 Dec 2011 09:10:54 +0100
changeset 45785 192243fd94a5
parent 45783 3e8a2464f607 (current diff)
parent 45784 ddac6eb800c6 (diff)
child 45786 3f07a7a91180
merged
--- 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)
isabelle