Mercurial Mercurial > hg > nominal2 / 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.
alpha_eqvt_tac with prod_rel and prod_fv simps
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 06 May 2010 14:21:10 +0200
changeset 2077 85826b52fd9d
parent 2076 6cb1a4639521
child 2078 1bebf8007677
alpha_eqvt_tac with prod_rel and prod_fv simps
Nominal/Rsp.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2