[isabelle-dev] NEWS

[Makarius]

* Document preparation: antiquotation @{lemma} now imitates a regular 
terminal proof, demanding keyword 'by' and supporting the full method 
expression syntax.

* ML antiquotations: block-structured compilation context indicated by
\<lbrace> ... \<rbrace>; additional antiquotation forms:
 
  @{let ?pat = term}                    - term abbreviation (HO matching)
  @{note name = fact}                   - fact abbreviation
  @{thm fact}                           - singleton fact (with attributes)
  @{thms fact}                          - general fact (with attributes)
  @{lemma prop by method}               - singleton goal
  @{lemma prop1 ... propN by method}    - general goal