Re: [isabelle] universal quantifiers vs. schematic variables
On 04.10.2015 20:02, David Cock wrote:
> You'll probably get answers from more knowledgable persons than I, but
> you've just discovered one of Isabelle's most fundamental quirks. As
> theorems, you're right that they're (logically) equivalent, but they
> differ if they appear as assumptions i.e.
Schematic variables are equivalent to outermost universal quantifiers.
> (!x. P x) => P y
> holds, but
> P ?x => P y
That is, the theorem "P ?x ==> P y" is equivalent to the theorem "!!x. P
x ==> P y" which is equivalent (in HOL) to "(?x. P x) ==> P y".
This archive was generated by a fusion of
Pipermail (Mailman edition) and