Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Rsp.thy
changeset 1673 e8cf0520c820
parent 1672 94b8b70f7bc0
child 1681 b8a07a3c1692 
--- a/Nominal/Rsp.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -62,7 +62,7 @@
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) 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
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
@@ -81,7 +81,7 @@
   simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
-   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
      @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
@@ -260,7 +260,7 @@
 
 ML {*
 fun fvbv_rsp_tac' simps ctxt =
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) 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} @ simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
nominal2