src/Provers/hypsubst.ML
changeset 646 7928c9760667
parent 231 cb6a24451544
child 680 f9e24455bbd1
     1.1 --- a/src/Provers/hypsubst.ML	Wed Oct 19 09:44:31 1994 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Oct 19 09:48:13 1994 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title: 	Provers/hypsubst
     1.5      ID:         $Id$
     1.6 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10  Martin Coen's tactic for substitution in the hypotheses
    1.11 @@ -49,6 +49,7 @@
    1.12  
    1.13  (*It's not safe to substitute for a constant; consider 0=1.
    1.14    It's not safe to substitute for x=t[x] since x is not eliminated.
    1.15 +  It's not safe to substitute for a Var; what if it appears in other goals?
    1.16    It's not safe to substitute for a variable free in the premises,
    1.17      but how could we check for this?*)
    1.18  fun inspect_pair bnd (t,u) =