# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273148470 -7200
# Node ID 85826b52fd9db073144690a9485bb605f469673f
# Parent  6cb1a463952172535d75a291f4eef185750f0290
alpha_eqvt_tac with prod_rel and prod_fv simps

diff -r 6cb1a4639521 -r 85826b52fd9d Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu May 06 14:14:30 2010 +0200
+++ b/Nominal/Rsp.thy	Thu May 06 14:21:10 2010 +0200
@@ -101,7 +101,7 @@
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW