# 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*)