equal
deleted
inserted
replaced
45 val mk_meta_prems = |
45 val mk_meta_prems = |
46 rule_by_tactic |
46 rule_by_tactic |
47 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
47 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
48 |
48 |
49 (*Congruence rules for = or <-> (instead of ==)*) |
49 (*Congruence rules for = or <-> (instead of ==)*) |
50 fun mk_meta_cong rl = |
50 fun mk_meta_cong (_: simpset) rl = |
51 Drule.export_without_context(mk_meta_eq (mk_meta_prems rl)) |
51 Drule.export_without_context(mk_meta_eq (mk_meta_prems rl)) |
52 handle THM _ => |
52 handle THM _ => |
53 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
53 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
54 |
54 |
55 |
55 |
69 val LK_basic_ss = |
69 val LK_basic_ss = |
70 Simplifier.global_context @{theory} empty_ss |
70 Simplifier.global_context @{theory} empty_ss |
71 setsubgoaler asm_simp_tac |
71 setsubgoaler asm_simp_tac |
72 setSSolver (mk_solver "safe" safe_solver) |
72 setSSolver (mk_solver "safe" safe_solver) |
73 setSolver (mk_solver "unsafe" unsafe_solver) |
73 setSolver (mk_solver "unsafe" unsafe_solver) |
74 setmksimps (map mk_meta_eq o atomize o gen_all) |
74 setmksimps (K (map mk_meta_eq o atomize o gen_all)) |
75 setmkcong mk_meta_cong; |
75 setmkcong mk_meta_cong; |
76 |
76 |
77 val LK_simps = |
77 val LK_simps = |
78 [triv_forall_equality, (* prunes params *) |
78 [triv_forall_equality, (* prunes params *) |
79 @{thm refl} RS @{thm P_iff_T}] @ |
79 @{thm refl} RS @{thm P_iff_T}] @ |