equal
deleted
inserted
replaced
277 |
277 |
278 |
278 |
279 (* atomize meta-connectives *) |
279 (* atomize meta-connectives *) |
280 |
280 |
281 fun rewrite_goal_tac rews = |
281 fun rewrite_goal_tac rews = |
282 Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews); |
282 Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews); |
283 |
283 |
284 fun atomize_tac rews = |
284 fun atomize_tac rews = |
285 let val rew_tac = rewrite_goal_tac rews in |
285 let val rew_tac = rewrite_goal_tac rews in |
286 fn i => fn thm => |
286 fn i => fn thm => |
287 if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then rew_tac i thm |
287 if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then rew_tac i thm |