1.1 --- a/src/Pure/Isar/method.ML	Fri Nov 02 18:53:00 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Nov 02 18:53:01 2007 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4    val trace: Proof.context -> thm list -> unit
     1.5    val rule_tac: thm list -> thm list -> int -> tactic
     1.6    val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
     1.7 +  val intros_tac: thm list -> thm list -> tactic
     1.8    val rule: thm list -> method
     1.9    val erule: int -> thm list -> method
    1.10    val drule: int -> thm list -> method
    1.11 @@ -288,6 +289,14 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(* intros_tac -- pervasive search spanned by intro rules *)
    1.16 +
    1.17 +fun intros_tac intros facts =
    1.18 +  ALLGOALS (insert_tac facts THEN'
    1.19 +      REPEAT_ALL_NEW (resolve_tac intros))
    1.20 +    THEN Tactic.distinct_subgoals_tac;
    1.21 +
    1.22 +
    1.23  (* iprover -- intuitionistic proof search *)
    1.24  
    1.25  local