Dear all, I have written a short note with a proposal for a _syntax for binders_ in Mizar (which I think is one of the things of which I think that it would improve Mizar most): http://www.cs.kun.nl/~freek/notes/binder.ps.gz Maybe it's useful to have a discussion about this? Freek