[isabelle-dev] NEWS

[Makarius]

* Pure/Isar: unified syntax for new-style specification mechanisms (e.g.
'definition', 'abbreviation', or 'inductive' in HOL) admits full type
inference and dummy patterns ("_"). For example:

  definition "K x _ = x"