equal
deleted
inserted
replaced
71 Goal.prove_global (Thm.theory_of_thm st) [] |
71 Goal.prove_global (Thm.theory_of_thm st) [] |
72 [mk_simp_implies @{prop "(x::'a) == y"}] |
72 [mk_simp_implies @{prop "(x::'a) == y"}] |
73 (mk_simp_implies @{prop "(x::'a) = y"}) |
73 (mk_simp_implies @{prop "(x::'a) = y"}) |
74 (fn {context = ctxt, prems} => EVERY |
74 (fn {context = ctxt, prems} => EVERY |
75 [rewrite_goals_tac ctxt @{thms simp_implies_def}, |
75 [rewrite_goals_tac ctxt @{thms simp_implies_def}, |
76 REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} :: |
76 REPEAT (assume_tac ctxt 1 ORELSE |
77 map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)]) |
77 resolve_tac ctxt |
|
78 (@{thm meta_eq_to_obj_eq} :: |
|
79 map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)]) |
78 end |
80 end |
79 end; |
81 end; |
80 |
82 |
81 (*Congruence rules for = (instead of ==)*) |
83 (*Congruence rules for = (instead of ==)*) |
82 fun mk_meta_cong ctxt rl = |
84 fun mk_meta_cong ctxt rl = |