Re: [isabelle] Lemma [OF ..] unification with \<And> parts
2013/5/13 Makarius <makarius at sketis.net>:
> On Sat, 11 May 2013, C. Diekmann wrote:
>> given these two lemmata
>> lemma l1: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E') ==> D"
>> lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
>> thm l1[OF l2]
>> I expected to get D. However, I get something very strange.
> As already pointed out by Larry, rule composition via "OF" (or "THEN" with
> different argument order), or "rule" as a proof method works exactly like
> that. You should study relevant Isabelle documentation until you expect the
> correct outcome and don't consider it to be strange. This is about
> higher-order natural deduction in Isabelle/Pure. Applications should not
> step out of that comfortable environment without good reason (which means
> you need to understand first what is its very purpose).
Thank you all for your answers. Today I learned that I want to use !
(∀), the ordinary FOL all quantifier.
This archive was generated by a fusion of
Pipermail (Mailman edition) and