src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Thu Sep 05 10:29:20 1996 +0200
+++ b/src/Pure/tactic.ML	Thu Sep 05 10:29:52 1996 +0200
@@ -247,6 +247,9 @@
 (*dresolve tactic applies a RULE to replace an assumption*)
 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
 
+(*Deletion of an assumption*)
+fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
+
 (*** Applications of cut_rl ***)
 
 (*Used by metacut_tac*)