equal
deleted
inserted
replaced
81 simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW |
81 simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW |
82 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
82 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
83 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
83 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
84 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
84 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
86 @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
86 @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
87 )) |
87 )) |
88 *} |
88 *} |
89 |
89 |
90 ML {* |
90 ML {* |
91 fun perm_arg arg = |
91 fun perm_arg arg = |