--- a/src/Pure/tactic.ML Fri Oct 27 15:23:39 2000 +0200
+++ b/src/Pure/tactic.ML Fri Oct 27 15:53:47 2000 +0200
@@ -96,6 +96,7 @@
val term_lift_inst_rule :
thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm
-> thm
+ val instantiate_tac : (string * string) list -> tactic
val thin_tac : string -> int -> tactic
val trace_goalno_tac : (int -> tactic) -> int -> tactic
end;
@@ -305,6 +306,9 @@
(*dresolve tactic applies a RULE to replace an assumption*)
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
+(*instantiate variables in the whole state*)
+val instantiate_tac = PRIMITIVE o read_instantiate;
+
(*Deletion of an assumption*)
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;