Re: [mizar] Scheme for func definition with Fraenkel operator?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Grzegorz (and others who answered my question),

I just hadn't realized that it's not a simple matter of
having a single scheme.  Thanks for all the answers.

>It will be nice to have the schemes and theorems
>automatically.  However, I do not thing we should work on it

I agree that it's not a very important thing.  (But I'm
curious, what is important according to you?  The thing I
would like to be worked on would be to get rid of the
"non-clusterable attributes", mainly because I don't know
what they are...)

Something related that _would_ be nice is to have "by"
strengthened in a way that:

  a in { x : P[x] } 

implies

  P[a]

instead of only

  ex x st a = x & P[x]

The current behavior is not very intuitive...  I have no idea
how to do this, though.

Freek