# 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.