Declared thin_tac
authorpaulson
Thu Sep 05 10:29:52 1996 +0200 (1996-09-05)
changeset 1951f2b8005bdc6e
parent 1950 97f1c6bf3ace
child 1952 4acc84e5831f
Declared thin_tac
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Sep 05 10:29:20 1996 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Sep 05 10:29:52 1996 +0200
     1.3 @@ -247,6 +247,9 @@
     1.4  (*dresolve tactic applies a RULE to replace an assumption*)
     1.5  fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
     1.6  
     1.7 +(*Deletion of an assumption*)
     1.8 +fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
     1.9 +
    1.10  (*** Applications of cut_rl ***)
    1.11  
    1.12  (*Used by metacut_tac*)