renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
authorwenzelm
Wed Mar 04 00:05:20 2009 +0100 (2009-03-04)
changeset 302347dd251bce291
parent 30233 6eb726e43ed1
child 30236 e70dae49dc57
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
src/Pure/Isar/method.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Mar 03 21:53:52 2009 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 04 00:05:20 2009 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    val atomize: bool -> method
     1.5    val this: method
     1.6    val fact: thm list -> Proof.context -> method
     1.7 -  val assumption_tac: Proof.context -> int -> tactic
     1.8 +  val assm_tac: Proof.context -> int -> tactic
     1.9    val assumption: Proof.context -> method
    1.10    val close: bool -> Proof.context -> method
    1.11    val trace: Proof.context -> thm list -> unit
    1.12 @@ -224,20 +224,20 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun assumption_tac ctxt =
    1.17 +fun assm_tac ctxt =
    1.18    assume_tac APPEND'
    1.19    Goal.assume_rule_tac ctxt APPEND'
    1.20    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    1.21    cond_rtac (can Logic.dest_term) Drule.termI;
    1.22  
    1.23  fun assumption ctxt = METHOD (HEADGOAL o
    1.24 -  (fn [] => assumption_tac ctxt
    1.25 +  (fn [] => assm_tac ctxt
    1.26      | [fact] => solve_tac [fact]
    1.27      | _ => K no_tac));
    1.28  
    1.29  fun close immed ctxt = METHOD (K
    1.30    (FILTER Thm.no_prems
    1.31 -    ((if immed then ALLGOALS (assumption_tac ctxt) else all_tac) THEN flexflex_tac)));
    1.32 +    ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
    1.33  
    1.34  end;
    1.35  
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 21:53:52 2009 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Mar 04 00:05:20 2009 +0100
     2.3 @@ -169,8 +169,7 @@
     2.4      fun try_thm thm =
     2.5        if Thm.no_prems thm then rtac thm 1 goal
     2.6        else (etacn thm THEN_ALL_NEW
     2.7 -             (Goal.norm_hhf_tac THEN'
     2.8 -               Method.assumption_tac ctxt)) 1 goal;
     2.9 +             (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
    2.10    in
    2.11      fn (_, thm) =>
    2.12        if (is_some o Seq.pull o try_thm) thm