Re: [isabelle] A course based on Isabelle/HOL and some feedback...
Probably you just need parentheses: (% x. f x) = (% y. f y)
The scope of a variable-binding operator is unlimited in both directions (left and right). This is a peculiarity of Isabelle's parser.
On 21 May 2012, at 06:38, Charlie (Cheolgi) Kim wrote:
> Thank you for the good resource.
> Indeed, I am using the material to teach myself Isabelle. The material is
> However, I found that myself cannot solve an exercise:
> Prove a property of the %-calculus: % x. f x = % y. f y
> which looks trivial, but whatever I try to make a lemma, they make syntax
> Can anybody guide me?
This archive was generated by a fusion of
Pipermail (Mailman edition) and