1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 14 23:19:51 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 14 23:19:57 2008 +0200
     1.3 @@ -307,26 +307,27 @@
     1.4  
     1.5    \item [@{method rule_tac} etc.] do resolution of rules with explicit
     1.6    instantiation.  This works the same way as the ML tactics @{ML
     1.7 -  res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}).
     1.8 +  Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
     1.9  
    1.10    Multiple rules may be only given if there is no instantiation; then
    1.11    @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
    1.12    \cite[\S3]{isabelle-ref}).
    1.13  
    1.14    \item [@{method cut_tac}] inserts facts into the proof state as
    1.15 -  assumption of a subgoal, see also @{ML cut_facts_tac} in
    1.16 +  assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
    1.17    \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
    1.18    variables is spread over the main goal statement.  Instantiations
    1.19 -  may be given as well, see also ML tactic @{ML cut_inst_tac} in
    1.20 -  \cite[\S3]{isabelle-ref}.
    1.21 +  may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
    1.22 +  in \cite[\S3]{isabelle-ref}.
    1.23  
    1.24    \item [@{method thin_tac}~@{text \<phi>}] deletes the specified
    1.25    assumption from a subgoal; note that @{text \<phi>} may contain schematic
    1.26 -  variables.  See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
    1.27 +  variables.  See also @{ML Tactic.thin_tac} in
    1.28 +  \cite[\S3]{isabelle-ref}.
    1.29  
    1.30    \item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
    1.31 -  assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
    1.32 -  subgoals_tac} in \cite[\S3]{isabelle-ref}.
    1.33 +  assumption to a subgoal.  See also @{ML Tactic.subgoal_tac} and @{ML
    1.34 +  Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
    1.35  
    1.36    \item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
    1.37    parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,

     2.1 --- a/src/Pure/tactic.ML	Sat Jun 14 23:19:51 2008 +0200
     2.2 +++ b/src/Pure/tactic.ML	Sat Jun 14 23:19:57 2008 +0200
     2.3 @@ -39,19 +39,9 @@
     2.4    val lift_inst_rule: thm * int * (string*string)list * thm -> thm
     2.5    val term_lift_inst_rule:
     2.6      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
     2.7 -  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
     2.8 -  val res_inst_tac: (string * string) list -> thm -> int -> tactic
     2.9 -  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    2.10 -  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    2.11 -  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    2.12 -  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    2.13 -  val instantiate_tac: (string * string) list -> tactic
    2.14 -  val thin_tac: string -> int -> tactic
    2.15    val metacut_tac: thm -> int -> tactic
    2.16    val cut_rules_tac: thm list -> int -> tactic
    2.17    val cut_facts_tac: thm list -> int -> tactic
    2.18 -  val subgoal_tac: string -> int -> tactic
    2.19 -  val subgoals_tac: string list -> int -> tactic
    2.20    val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
    2.21    val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
    2.22      bool -> 'a Net.net * 'a Net.net -> int -> tactic
    2.23 @@ -82,11 +72,21 @@
    2.24    include BASIC_TACTIC
    2.25    val innermost_params: int -> thm -> (string * typ) list
    2.26    val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
    2.27 +  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
    2.28 +  val res_inst_tac: (string * string) list -> thm -> int -> tactic
    2.29 +  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    2.30 +  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    2.31 +  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    2.32 +  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    2.33 +  val instantiate_tac: (string * string) list -> tactic
    2.34    val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
    2.35    val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
    2.36    val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
    2.37    val make_elim_preserve: thm -> thm
    2.38    val instantiate_tac': (indexname * string) list -> tactic
    2.39 +  val thin_tac: string -> int -> tactic
    2.40 +  val subgoal_tac: string -> int -> tactic
    2.41 +  val subgoals_tac: string list -> int -> tactic
    2.42    val untaglist: (int * 'a) list -> 'a list
    2.43    val orderlist: (int * 'a) list -> 'a list
    2.44    val insert_tagged_brl: 'a * (bool * thm) ->