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.

Larry Paulson


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
> awesome.
> 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
> errors.
> 
> Can anybody guide me?






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