src/Pure/Isar/method.ML

   val close: bool -> Proof.context -> method
   val trace: Proof.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
   val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   val intros_tac: thm list -> thm list -> tactic
+  val try_intros_tac: thm list -> thm list -> tactic
   val rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
   val frule: int -> thm list -> method
   val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context

 end;
 
 
 (* intros_tac -- pervasive search spanned by intro rules *)
 
-fun intros_tac intros facts =
-  ALLGOALS (insert_tac facts THEN'
+fun gen_intros_tac goals intros facts =
+  goals (insert_tac facts THEN'
       REPEAT_ALL_NEW (resolve_tac intros))
     THEN Tactic.distinct_subgoals_tac;
 
+val intros_tac = gen_intros_tac ALLGOALS;
+val try_intros_tac = gen_intros_tac TRYALL;
 
 (* ML tactics *)
 
 structure TacticData = Proof_Data
 (