src/Pure/Isar/rule_insts.ML
changeset 27219 a248dba028ff
parent 27120 b21eec437295
child 27236 80356567e7ad
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Jun 14 23:20:11 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 14 23:20:12 2008 +0200
     1.3 @@ -11,6 +11,9 @@
     1.4      thm -> int -> tactic
     1.5    val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
     1.6    val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
     1.7 +  val subgoal_tac: Proof.context -> string -> int -> tactic
     1.8 +  val subgoals_tac: Proof.context -> string list -> int -> tactic
     1.9 +  val thin_tac: Proof.context -> string -> int -> tactic
    1.10  end;
    1.11  
    1.12  structure RuleInsts: RULE_INSTS =