Re: [Hol-info] Rewriting bug in HOL Light?

[Rob A. <rd...@le...>]

On Thursday 02 Feb 2006 3:21 pm, John Harrison wrote:

>...
> No, this is standard behaviour in all versions of HOL as far as I know.
> Free variables in a theorem are effectively universally quantified and
> can be instantiated to anything.
>

Not in ProofPower-HOL. We thought it would give a useful extra bit of control 
only to instantiate variables bound by an outermost universal quantifier in 
the rewrite theorems. This does what Stephen was expecting.

I think it's also a little faster (assuming your logical logical kernel will 
instantiate a universal quantification without processing the assumptions of 
the theorem).

Regards,

Rob.