[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sat Jun 28 22:59:51 CEST 2008

* 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

More information about the isabelle-dev mailing list