[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Lawrence Paulson]

I'd prefer to keep things simple. I do like your recent syntactic innovations, but such things need to be introduced with care. And the inner syntax is considerably more delicate.
Larry

> On 2 Feb 2018, at 10:50, Makarius <makarius at sketis.net> wrote:
> 
> The general concept behind it is implicit abstraction, here with
> explicit (( ... )) to delimit its scope (different notation would be
> required in reality):
> 
>  ((a + _))  ~> %x. a + x
>  ((_ + a))  ~> %x. x + a
>  ((a + _ + b + _))  ~>  %x y. a + x + b + y
>  ((_ < a))  ~> %x. x < a
> 
> E.g.
> 
>  filter ((_ < a)) list
>  map ((_ - a)) list
>  All ((_ < a))
>  Collect ((_ < a))
> 
> We already have implicit underscore treatment for clausal definitions,
> so the above would not be totally alien. (But I am not proposing to do
> anything concrete now.)