src/Provers/hypsubst.ML
changeset 4299 22596d62ce0b
parent 4223 f60e3d2c81d3
child 4466 305390f23734
     1.1 --- a/src/Provers/hypsubst.ML	Wed Nov 26 16:48:11 1997 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 26 16:49:07 1997 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4    When can we safely delete the equality?
     1.5      Not if it equates two constants; consider 0=1.
     1.6      Not if it resembles x=t[x], since substitution does not eliminate x.
     1.7 -    Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
     1.8 +    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
     1.9      Not if it involves a variable free in the premises, 
    1.10          but we can't check for this -- hence bnd and bound_hyp_subst_tac
    1.11    Prefer to eliminate Bound variables if possible.