changeset 16647 | c6d81ddebb0e |
parent 16417 | 9bc16273c2d4 |
child 27682 | 25aceefd4786 |
--- 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