equal
deleted
inserted
replaced
47 rule_by_tactic |
47 rule_by_tactic |
48 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
48 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
49 |
49 |
50 (*Congruence rules for = or <-> (instead of ==)*) |
50 (*Congruence rules for = or <-> (instead of ==)*) |
51 fun mk_meta_cong rl = |
51 fun mk_meta_cong rl = |
52 Drule.standard(mk_meta_eq (mk_meta_prems rl)) |
52 Drule.export_without_context(mk_meta_eq (mk_meta_prems rl)) |
53 handle THM _ => |
53 handle THM _ => |
54 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
54 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
55 |
55 |
56 |
56 |
57 (*** Standard simpsets ***) |
57 (*** Standard simpsets ***) |
58 |
58 |
59 val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, |
59 val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, |