|
From: Rob A. <rd...@le...> - 2006-02-02 16:44:08
|
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. |