equal
deleted
inserted
replaced
929 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
929 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
930 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
930 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
931 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
931 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
932 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
932 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
933 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
933 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
934 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
934 simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW |
935 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
935 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
936 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
936 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
937 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
937 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
938 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
938 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
939 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
939 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |