# HG changeset patch
# User haftmann
# Date 1194025981 -3600
# Node ID 2ed7b34f58e6d510608c9d4de39b0eab527044f6
# Parent  f9090ae5cec9f3183c2f6023f8d0301f575c6c2b
generic tactic Method.intros_tac

diff -r f9090ae5cec9 -r 2ed7b34f58e6 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:00 2007 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:01 2007 +0100
@@ -1955,9 +1955,7 @@
     val thy = ProofContext.theory_of ctxt;
     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
   in
-    (ALLGOALS (Method.insert_tac facts THEN'
-        REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
-      THEN Tactic.distinct_subgoals_tac) st
+    Method.intros_tac (wits @ intros) facts st
   end;
 
 val _ = Context.add_setup (Method.add_methods
diff -r f9090ae5cec9 -r 2ed7b34f58e6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Nov 02 18:53:00 2007 +0100
+++ b/src/Pure/Isar/method.ML	Fri Nov 02 18:53:01 2007 +0100
@@ -45,6 +45,7 @@
   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 rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
@@ -288,6 +289,14 @@
 end;
 
 
+(* intros_tac -- pervasive search spanned by intro rules *)
+
+fun intros_tac intros facts =
+  ALLGOALS (insert_tac facts THEN'
+      REPEAT_ALL_NEW (resolve_tac intros))
+    THEN Tactic.distinct_subgoals_tac;
+
+
 (* iprover -- intuitionistic proof search *)
 
 local