equal
deleted
inserted
replaced
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 (@{thm 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 |
904 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
904 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |