equal
deleted
inserted
replaced
219 (ccs ~~ (map (map atomic o prems_of) congs)); |
219 (ccs ~~ (map (map atomic o prems_of) congs)); |
220 in add_norms(congs,ccs,new_asms) end; |
220 in add_norms(congs,ccs,new_asms) end; |
221 |
221 |
222 fun normed_rews congs = |
222 fun normed_rews congs = |
223 let val add_norms = add_norm_tags congs in |
223 let val add_norms = add_norm_tags congs in |
224 fn thm => Variable.tradeT |
224 fn thm => |
225 (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm] |
225 let |
|
226 val ctxt = |
|
227 Thm.theory_of_thm thm |
|
228 |> Proof_Context.init_global |
|
229 |> Variable.declare_thm thm; |
|
230 in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end |
226 end; |
231 end; |
227 |
232 |
228 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
233 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
229 |
234 |
230 val trans_norms = map mk_trans normE_thms; |
235 val trans_norms = map mk_trans normE_thms; |