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/Fv.thy
changeset 1672 94b8b70f7bc0
parent 1670 ed89a26b7074
child 1673 e8cf0520c820 
--- a/Nominal/Fv.thy	Sat Mar 27 08:11:45 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:17:43 2010 +0100
@@ -653,7 +653,7 @@
   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
 
@@ -898,7 +898,7 @@
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
nominal2