Re: [isabelle] universal quantifiers vs. schematic variables
Grr, sorry, hit send without proofreading. That second one should have
P x => P y
i.e. an *unbound*, not a schematic name.
Noam: in your example, it's not clear whether you have an actual
schematic, or just an unbound (blue) variable.
On 04/10/15 11:19, Jasmin Blanchette wrote:
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.
(!x. P x) => P y
P ?x => P y
does not (necessarily) hold.
schematic_lemma "P ?x ==> P y"
This archive was generated by a fusion of
Pipermail (Mailman edition) and