# HG changeset patch
# User paulson
# Date 841912192 -7200
# Node ID f2b8005bdc6e721327c4b5f85812d4a6423a34a5
# Parent  97f1c6bf3acece774a8418b7842401d73400b560
Declared thin_tac

diff -r 97f1c6bf3ace -r f2b8005bdc6e 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*)