added atomize_goal / atomize_tac;
authorwenzelm
Tue Aug 01 11:55:27 2000 +0200 (2000-08-01)
changeset 9485e56577a63005
parent 9484 3bda55143260
child 9486 2df511ebb956
added atomize_goal / atomize_tac;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Aug 01 00:20:12 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Aug 01 11:55:27 2000 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val unfold: thm list -> Proof.method
     1.5    val fold: thm list -> Proof.method
     1.6    val atomize_tac: thm list -> int -> tactic
     1.7 +  val atomize_goal: thm list -> int -> thm -> thm
     1.8    val multi_resolve: thm list -> thm -> thm Seq.seq
     1.9    val multi_resolves: thm list -> thm list -> thm Seq.seq
    1.10    val resolveq_tac: thm Seq.seq -> int -> tactic
    1.11 @@ -252,11 +253,15 @@
    1.12  
    1.13  (* atomize meta-connectives *)
    1.14  
    1.15 -fun atomize_tac rews i st =
    1.16 -  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
    1.17 -    (warning "FIXME: atomize_tac";
    1.18 -    Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i st)
    1.19 -  else all_tac st;
    1.20 +fun atomize_tac rews i thm =
    1.21 +  if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then
    1.22 +    Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i thm
    1.23 +  else all_tac thm;
    1.24 +
    1.25 +fun atomize_goal rews i thm =
    1.26 +  (case Seq.pull (atomize_tac rews i thm) of
    1.27 +    None => thm
    1.28 +  | Some (thm', _) => thm');
    1.29  
    1.30  
    1.31  (* multi_resolve *)