equal
deleted
inserted
replaced
142 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
142 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
143 |
143 |
144 |
144 |
145 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
145 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
146 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
146 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
147 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def |
147 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
148 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
148 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
149 |
149 |
150 fun p_tac msg i = |
150 fun p_tac msg i = |
151 if false then print_tac ("ptest: " ^ msg) else all_tac |
151 if false then print_tac ("ptest: " ^ msg) else all_tac |
152 |
152 |