Re: [isabelle] Variable names



On Wed, 7 Feb 2007, Tom Ridge wrote:

> We used to write e.g. (% v_. P v_)
> 
> But with recent development versions of Isabelle, it appears user 
> variable names are not allowed to end with an underscore.

Trailing underscore have been reserved for internal use many years ago, 
although not all parts of the system have treated this uniformly.  
Lambda-bound variables have been included in this general scheme recently, 
motivated by a more serious treatment of %_. b where the body does not 
mention the bound variable.


> We have lots of code that would need to be updated to track this change.

You can add further decorations to prevent the last character being an 
underscore, e.g. x_'


	Makarius





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