Re: [isabelle] universal quantifiers vs. schematic variables



David,

> 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
> 
> holds, but
> 
> P ?x => P y
> 
> does not (necessarily) hold.

Huh?

schematic_lemma "P ?x ==> P y"
  by assumption

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.