# HG changeset patch
# User berghofe
# Date 1120220192 -7200
# Node ID c6d81ddebb0e9adfec3357fea8c3b909b6869816
# Parent  666774b0d1b0c7da29699b5f6fa77aab81b18e8a
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.

diff -r 666774b0d1b0 -r c6d81ddebb0e src/HOL/UNITY/Guar.thy
--- 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