generic tactic Method.intros_tac
authorhaftmann
Fri Nov 02 18:53:01 2007 +0100 (2007-11-02)
changeset 252702ed7b34f58e6
parent 25269 f9090ae5cec9
child 25271 f28efd37e18a
generic tactic Method.intros_tac
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:00 2007 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:01 2007 +0100
     1.3 @@ -1955,9 +1955,7 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
     1.6    in
     1.7 -    (ALLGOALS (Method.insert_tac facts THEN'
     1.8 -        REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
     1.9 -      THEN Tactic.distinct_subgoals_tac) st
    1.10 +    Method.intros_tac (wits @ intros) facts st
    1.11    end;
    1.12  
    1.13  val _ = Context.add_setup (Method.add_methods
     2.1 --- a/src/Pure/Isar/method.ML	Fri Nov 02 18:53:00 2007 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Fri Nov 02 18:53:01 2007 +0100
     2.3 @@ -45,6 +45,7 @@
     2.4    val trace: Proof.context -> thm list -> unit
     2.5    val rule_tac: thm list -> thm list -> int -> tactic
     2.6    val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
     2.7 +  val intros_tac: thm list -> thm list -> tactic
     2.8    val rule: thm list -> method
     2.9    val erule: int -> thm list -> method
    2.10    val drule: int -> thm list -> method
    2.11 @@ -288,6 +289,14 @@
    2.12  end;
    2.13  
    2.14  
    2.15 +(* intros_tac -- pervasive search spanned by intro rules *)
    2.16 +
    2.17 +fun intros_tac intros facts =
    2.18 +  ALLGOALS (insert_tac facts THEN'
    2.19 +      REPEAT_ALL_NEW (resolve_tac intros))
    2.20 +    THEN Tactic.distinct_subgoals_tac;
    2.21 +
    2.22 +
    2.23  (* iprover -- intuitionistic proof search *)
    2.24  
    2.25  local