| changeset 42815 | 61668e617a3b |
| parent 42809 | 5b45125b15ba |
| child 42843 | 0e594ba0b324 |
--- 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.