1.1 --- a/NEWS	Sun May 15 17:45:53 2011 +0200
     1.2 +++ b/NEWS	Sun May 15 18:00:08 2011 +0200
     1.3 @@ -58,6 +58,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Declare ext [intro] by default.  Rare INCOMPATIBILITY.
     1.8 +
     1.9  * Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
    1.10  interpretation proofs may need adjustment.  INCOMPATIBILITY.
    1.11