Re: [isabelle] Matching done by the transfer method



> "(λ Q. (∀ x>0. Q x)) (λx. P x)" and "∀ x>0. P x" are not exactly the same.
> They are only beta-equivalent. And you should know that when a term is
> parsed in Isabelle, it's beta-normalized. Thus your goal is really this
> term "∀ x>0. P x".
>
>
 I see. Thanks. Then I'll find my way around this using tricks like Ball,
or defining my own bounded quantifiers when I need them.



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