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.
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
authorberghofe
Fri, 01 Jul 2005 14:16:32 +0200
changeset 16647 c6d81ddebb0e
parent 16646 666774b0d1b0
child 16648 fc2a425f0977
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
src/HOL/UNITY/Guar.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 01 14:14:40 2005 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 01 14:16:32 2005 +0200
@@ -431,7 +431,7 @@
 by (unfold wx_def, auto)
 
 lemma wx_ex_prop: "ex_prop (wx X)"
-apply (simp add: wx_def ex_prop_equiv, safe, blast)
+apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
 apply force 
 done
isabelle