1.1 --- a/NEWS	Fri Apr 27 20:57:40 2012 +0200
     1.2 +++ b/NEWS	Fri Apr 27 21:02:34 2012 +0200
     1.3 @@ -9,15 +9,16 @@
     1.4  * Prover IDE (PIDE) improvements:
     1.5  
     1.6    - more robust Sledgehammer integration (as before the sledgehammer
     1.7 -    command line needs to be typed into the source buffer)
     1.8 +    command-line needs to be typed into the source buffer)
     1.9    - markup for bound variables
    1.10 -  - markup for types of term variables (e.g. displayed as tooltips)
    1.11 +  - markup for types of term variables (displayed as tooltips)
    1.12    - support for user-defined Isar commands within the running session
    1.13    - improved support for Unicode outside original 16bit range
    1.14      e.g. glyph for \<A> (thanks to jEdit 4.5.1)
    1.15  
    1.16 -* Updated and extended reference manuals ("isar-ref" and
    1.17 -"implementation"); reduced remaining material in old "ref" manual.
    1.18 +* Forward declaration of outer syntax keywords within the theory
    1.19 +header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
    1.20 +commands to be used in the same theory where defined.
    1.21  
    1.22  * Rule attributes in local theory declarations (e.g. locale or class)
    1.23  are now statically evaluated: the resulting theorem is stored instead
    1.24 @@ -31,23 +32,12 @@
    1.25  becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    1.26  indices of schematic variables.
    1.27  
    1.28 -* Renamed some inner syntax categories:
    1.29 -
    1.30 -    num ~> num_token
    1.31 -    xnum ~> xnum_token
    1.32 -    xstr ~> str_token
    1.33 -
    1.34 -Minor INCOMPATIBILITY.  Note that in practice "num_const" or
    1.35 -"num_position" etc. are mainly used instead (which also include
    1.36 -position information via constraints).
    1.37 -
    1.38  * Simplified configuration options for syntax ambiguity: see
    1.39  "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.40  manual.  Minor INCOMPATIBILITY.
    1.41  
    1.42 -* Forward declaration of outer syntax keywords within the theory
    1.43 -header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
    1.44 -commands to be used in the same theory where defined.
    1.45 +* Updated and extended reference manuals: "isar-ref" and
    1.46 +"implementation"; reduced remaining material in old "ref" manual.
    1.47  
    1.48  
    1.49  *** Pure ***
    1.50 @@ -93,6 +83,16 @@
    1.51  into the user context.  Minor INCOMPATIBILITY, may use the regular
    1.52  "def" result with attribute "abs_def" to imitate the old version.
    1.53  
    1.54 +* Renamed some inner syntax categories:
    1.55 +
    1.56 +    num ~> num_token
    1.57 +    xnum ~> xnum_token
    1.58 +    xstr ~> str_token
    1.59 +
    1.60 +Minor INCOMPATIBILITY.  Note that in practice "num_const" or
    1.61 +"num_position" etc. are mainly used instead (which also include
    1.62 +position information via constraints).
    1.63 +
    1.64  * Attribute "abs_def" turns an equation of the form "f x y == t" into
    1.65  "f == %x y. t", which ensures that "simp" or "unfold" steps always
    1.66  expand it.  This also works for object-logic equality.  (Formerly
    1.67 @@ -131,13 +131,12 @@
    1.68  
    1.69  *** HOL ***
    1.70  
    1.71 -* New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").
    1.72 -It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
    1.73 -which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
    1.74 -for Higher-Order Logic" as the recommended beginners tutorial
    1.75 -but does not cover all of the material of that old tutorial.
    1.76 -
    1.77 -* Discontinued old Tutorial on Isar ("isar-overview");
    1.78 +* New tutorial "Programming and Proving in Isabelle/HOL"
    1.79 +("prog-prove").  It completely supersedes "A Tutorial Introduction to
    1.80 +Structured Isar Proofs" ("isar-overview"), which has been removed.  It
    1.81 +also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
    1.82 +Logic" as the recommended beginners tutorial, but does not cover all
    1.83 +of the material of that old tutorial.
    1.84  
    1.85  * Type 'a set is now a proper type constructor (just as before
    1.86  Isabelle2008).  Definitions mem_def and Collect_def have disappeared.