src/Provers/hypsubst.ML
 changeset 4299 22596d62ce0b parent 4223 f60e3d2c81d3 child 4466 305390f23734
equal inserted replaced
4298:b69eedd3aa6c 4299:22596d62ce0b
`    76 (*If novars then we forbid Vars in the equality.`
`    76 (*If novars then we forbid Vars in the equality.`
`    77   If bnd then we only look for Bound (or dotted Free) variables to eliminate. `
`    77   If bnd then we only look for Bound (or dotted Free) variables to eliminate. `
`    78   When can we safely delete the equality?`
`    78   When can we safely delete the equality?`
`    79     Not if it equates two constants; consider 0=1.`
`    79     Not if it equates two constants; consider 0=1.`
`    80     Not if it resembles x=t[x], since substitution does not eliminate x.`
`    80     Not if it resembles x=t[x], since substitution does not eliminate x.`
`    81     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)`
`    81     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P`
`    82     Not if it involves a variable free in the premises, `
`    82     Not if it involves a variable free in the premises, `
`    83         but we can't check for this -- hence bnd and bound_hyp_subst_tac`
`    83         but we can't check for this -- hence bnd and bound_hyp_subst_tac`
`    84   Prefer to eliminate Bound variables if possible.`
`    84   Prefer to eliminate Bound variables if possible.`
`    85   Result:  true = use as is,  false = reorient first *)`
`    85   Result:  true = use as is,  false = reorient first *)`
`    86 fun inspect_pair bnd novars (t,u,T) =`
`    86 fun inspect_pair bnd novars (t,u,T) =`