src/Pure/tactic.ML
changeset 27209 388fd72e9f26
parent 27158 113a32dd0b14
child 27243 d549b5b0f344
     1.1 --- a/src/Pure/tactic.ML	Sat Jun 14 23:19:51 2008 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Jun 14 23:19:57 2008 +0200
     1.3 @@ -39,19 +39,9 @@
     1.4    val lift_inst_rule: thm * int * (string*string)list * thm -> thm
     1.5    val term_lift_inst_rule:
     1.6      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
     1.7 -  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
     1.8 -  val res_inst_tac: (string * string) list -> thm -> int -> tactic
     1.9 -  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.10 -  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    1.11 -  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    1.12 -  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.13 -  val instantiate_tac: (string * string) list -> tactic
    1.14 -  val thin_tac: string -> int -> tactic
    1.15    val metacut_tac: thm -> int -> tactic
    1.16    val cut_rules_tac: thm list -> int -> tactic
    1.17    val cut_facts_tac: thm list -> int -> tactic
    1.18 -  val subgoal_tac: string -> int -> tactic
    1.19 -  val subgoals_tac: string list -> int -> tactic
    1.20    val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
    1.21    val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
    1.22      bool -> 'a Net.net * 'a Net.net -> int -> tactic
    1.23 @@ -82,11 +72,21 @@
    1.24    include BASIC_TACTIC
    1.25    val innermost_params: int -> thm -> (string * typ) list
    1.26    val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
    1.27 +  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
    1.28 +  val res_inst_tac: (string * string) list -> thm -> int -> tactic
    1.29 +  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.30 +  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    1.31 +  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    1.32 +  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.33 +  val instantiate_tac: (string * string) list -> tactic
    1.34    val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
    1.35    val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
    1.36    val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
    1.37    val make_elim_preserve: thm -> thm
    1.38    val instantiate_tac': (indexname * string) list -> tactic
    1.39 +  val thin_tac: string -> int -> tactic
    1.40 +  val subgoal_tac: string -> int -> tactic
    1.41 +  val subgoals_tac: string list -> int -> tactic
    1.42    val untaglist: (int * 'a) list -> 'a list
    1.43    val orderlist: (int * 'a) list -> 'a list
    1.44    val insert_tagged_brl: 'a * (bool * thm) ->