export subgoal_tac, subgoals_tac, thin_tac;
authorwenzelm
Sat Jun 14 23:20:12 2008 +0200 (2008-06-14 ago)
changeset 27219a248dba028ff
parent 27218 4548c83cd508
child 27220 31adee1f467a
export subgoal_tac, subgoals_tac, thin_tac;
src/Pure/Isar/rule_insts.ML
     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 =