equal
deleted
inserted
replaced
893 rel_indtac ind THEN_ALL_NEW |
893 rel_indtac ind THEN_ALL_NEW |
894 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
894 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
895 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW |
895 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW |
896 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
896 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
897 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
897 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
898 simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW |
898 simp_tac (HOL_basic_ss addsimps (@{thm permute_abs} :: perm)) THEN_ALL_NEW |
899 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
899 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
900 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
900 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
901 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
901 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
902 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
902 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
903 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
903 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |