Re: [isabelle] Very strange behaviour of interpretation



Hi Andreas,

since f is a new parameter, it must be fixed explicitly:

  interpretation itrprt: L "bar f" for f .

Tthen everything looks as expected.

I remember that there has been some discussion whether free variable
should be fixed automatically, but I on my behalf cannot tell what its
result are.

Hope this helps
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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