# HG changeset patch
# User wenzelm
# Date 1305475208 -7200
# Node ID 61668e617a3bab4f4c5a240f3c7121f4b611e38b
# Parent  5af15f1e2ef60b0bf864250e238a906973f29c7a
NEWS (cf. 4e8483cc2cc5);

diff -r 5af15f1e2ef6 -r 61668e617a3b NEWS
--- a/NEWS	Sun May 15 17:45:53 2011 +0200
+++ b/NEWS	Sun May 15 18:00:08 2011 +0200
@@ -58,6 +58,8 @@
 
 *** HOL ***
 
+* Declare ext [intro] by default.  Rare INCOMPATIBILITY.
+
 * Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
 interpretation proofs may need adjustment.  INCOMPATIBILITY.