equal
deleted
inserted
replaced
1089 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
1089 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
1090 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
1090 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
1091 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
1091 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
1092 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
1092 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
1093 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
1093 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
1094 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
1094 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
1095 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW |
|
1096 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
1095 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
1097 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
|
1098 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
1096 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
1099 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
1097 *} |
1100 *} |
1098 |
1101 |
1099 end |
1102 end |