src/Provers/hypsubst.ML
changeset 4223 f60e3d2c81d3
parent 4179 cc4b6791d5dc
child 4299 22596d62ce0b
     1.1 --- a/src/Provers/hypsubst.ML	Wed Nov 12 16:28:53 1997 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 12 18:58:50 1997 +0100
     1.3 @@ -3,8 +3,9 @@
     1.4      Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     1.5      Copyright   1995  University of Cambridge
     1.6  
     1.7 -Tactic to substitute using the assumption x=t in the rest of the subgoal,
     1.8 -and to delete that assumption.  Original version due to Martin Coen.
     1.9 +Tactic to substitute using (at least) the assumption x=t in the rest of the 
    1.10 +subgoal, and to delete (at least) that assumption. 
    1.11 +Original version due to Martin Coen.
    1.12  
    1.13  This version uses the simplifier, and requires it to be already present.
    1.14  
    1.15 @@ -31,7 +32,8 @@
    1.16    val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    1.17    val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    1.18    val sym	       : thm		   (* a=b ==> b=a *)
    1.19 -  end;
    1.20 +  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    1.21 +end;
    1.22  
    1.23  
    1.24  signature HYPSUBST =
    1.25 @@ -174,8 +176,8 @@
    1.26        handle THM _ => no_tac | EQ_VAR => no_tac);
    1.27  
    1.28  (*Substitutes for Free or Bound variables*)
    1.29 -val hyp_subst_tac = 
    1.30 -    gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;
    1.31 +val hyp_subst_tac = FIRST' [ematch_tac [thin_refl],
    1.32 +        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
    1.33  
    1.34  (*Substitutes for Bound variables only -- this is always safe*)
    1.35  val bound_hyp_subst_tac =