# HG changeset patch
# User wenzelm
# Date 1213478412 -7200
# Node ID a248dba028ffc27fdd8ea6347eb449746b107352
# Parent  4548c83cd5081b2a53e36d4a0feee30b35a941b2
export subgoal_tac, subgoals_tac, thin_tac;

diff -r 4548c83cd508 -r a248dba028ff src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Jun 14 23:20:11 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 14 23:20:12 2008 +0200
@@ -11,6 +11,9 @@
     thm -> int -> tactic
   val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
   val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val subgoal_tac: Proof.context -> string -> int -> tactic
+  val subgoals_tac: Proof.context -> string list -> int -> tactic
+  val thin_tac: Proof.context -> string -> int -> tactic
 end;
 
 structure RuleInsts: RULE_INSTS =