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.
prod_rel and prod_fv simps
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 06 May 2010 14:10:56 +0200
changeset 2072 db218886e674
parent 2071 843e0a2d44d7
child 2075 c1edd05f207f
prod_rel and prod_fv simps
Nominal/Rsp.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Rsp.thy	Thu May 06 14:10:26 2010 +0200
+++ b/Nominal/Rsp.thy	Thu May 06 14:10:56 2010 +0200
@@ -63,7 +63,7 @@
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps}))
   ))
 *}
nominal2