--- a/doc-src/IsarRef/Thy/Generic.thy Sat Jun 14 23:19:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sat Jun 14 23:19:57 2008 +0200
@@ -307,26 +307,27 @@
\item [@{method rule_tac} etc.] do resolution of rules with explicit
instantiation. This works the same way as the ML tactics @{ML
- res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}).
+ Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
Multiple rules may be only given if there is no instantiation; then
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
\cite[\S3]{isabelle-ref}).
\item [@{method cut_tac}] inserts facts into the proof state as
- assumption of a subgoal, see also @{ML cut_facts_tac} in
+ assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
\cite[\S3]{isabelle-ref}. Note that the scope of schematic
variables is spread over the main goal statement. Instantiations
- may be given as well, see also ML tactic @{ML cut_inst_tac} in
- \cite[\S3]{isabelle-ref}.
+ may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
+ in \cite[\S3]{isabelle-ref}.
\item [@{method thin_tac}~@{text \<phi>}] deletes the specified
assumption from a subgoal; note that @{text \<phi>} may contain schematic
- variables. See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
+ variables. See also @{ML Tactic.thin_tac} in
+ \cite[\S3]{isabelle-ref}.
\item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
- assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
- subgoals_tac} in \cite[\S3]{isabelle-ref}.
+ assumption to a subgoal. See also @{ML Tactic.subgoal_tac} and @{ML
+ Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
\item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
--- a/src/Pure/tactic.ML Sat Jun 14 23:19:51 2008 +0200
+++ b/src/Pure/tactic.ML Sat Jun 14 23:19:57 2008 +0200
@@ -39,19 +39,9 @@
val lift_inst_rule: thm * int * (string*string)list * thm -> thm
val term_lift_inst_rule:
thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
- val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
- val res_inst_tac: (string * string) list -> thm -> int -> tactic
- val eres_inst_tac: (string * string) list -> thm -> int -> tactic
- val cut_inst_tac: (string * string) list -> thm -> int -> tactic
- val forw_inst_tac: (string * string) list -> thm -> int -> tactic
- val dres_inst_tac: (string * string) list -> thm -> int -> tactic
- val instantiate_tac: (string * string) list -> tactic
- val thin_tac: string -> int -> tactic
val metacut_tac: thm -> int -> tactic
val cut_rules_tac: thm list -> int -> tactic
val cut_facts_tac: thm list -> int -> tactic
- val subgoal_tac: string -> int -> tactic
- val subgoals_tac: string list -> int -> tactic
val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
bool -> 'a Net.net * 'a Net.net -> int -> tactic
@@ -82,11 +72,21 @@
include BASIC_TACTIC
val innermost_params: int -> thm -> (string * typ) list
val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
+ val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
+ val res_inst_tac: (string * string) list -> thm -> int -> tactic
+ val eres_inst_tac: (string * string) list -> thm -> int -> tactic
+ val cut_inst_tac: (string * string) list -> thm -> int -> tactic
+ val forw_inst_tac: (string * string) list -> thm -> int -> tactic
+ val dres_inst_tac: (string * string) list -> thm -> int -> tactic
+ val instantiate_tac: (string * string) list -> tactic
val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
val make_elim_preserve: thm -> thm
val instantiate_tac': (indexname * string) list -> tactic
+ val thin_tac: string -> int -> tactic
+ val subgoal_tac: string -> int -> tactic
+ val subgoals_tac: string list -> int -> tactic
val untaglist: (int * 'a) list -> 'a list
val orderlist: (int * 'a) list -> 'a list
val insert_tagged_brl: 'a * (bool * thm) ->