# HG changeset patch # User wenzelm # Date 1003082999 -7200 # Node ID 4c45eb23ef68c1436ecb7713660513829c1a02ec # Parent fd780dd6e0b4b00032f281a0e2788a0c24f03a5c atomize_tac etc. moved to object_logic.ML; diff -r fd780dd6e0b4 -r 4c45eb23ef68 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Oct 14 20:09:19 2001 +0200 +++ b/src/Pure/Isar/method.ML Sun Oct 14 20:09:59 2001 +0200 @@ -41,9 +41,6 @@ val insert_facts: Proof.method val unfold: thm list -> Proof.method val fold: thm list -> Proof.method - val atomize_tac: thm list -> int -> tactic - val atomize_goal: thm list -> int -> thm -> thm - val atomize_strip_tac: thm list * thm list -> int -> tactic val multi_resolve: thm list -> thm -> thm Seq.seq val multi_resolves: thm list -> thm list -> thm Seq.seq val rule_tac: thm list -> thm list -> int -> tactic @@ -284,23 +281,6 @@ fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms)); -(* atomize meta-connectives *) - -fun atomize_strip_tac (rews, strip) = - let val rew_tac = rewrite_goal_tac rews in - fn i => fn thm => - if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then - (rew_tac i THEN REPEAT (match_tac strip i)) thm - else all_tac thm - end; - -fun atomize_tac rews = atomize_strip_tac (rews, []); - -fun atomize_goal rews = - let val tac = atomize_tac rews - in fn i => fn thm => (case Seq.pull (tac i thm) of None => thm | Some (thm', _) => thm') end; - - (* multi_resolve *) local