--- 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