| changeset 36093 | 0880493627ca |
| parent 34962 | 807f6ce0273d |
| child 36096 | abc6a2ea4b88 |
--- a/NEWS Mon Feb 15 01:27:06 2010 +0100 +++ b/NEWS Mon Feb 15 01:34:08 2010 +0100 @@ -9,6 +9,8 @@ * Code generator: details of internal data cache have no impact on the user space functionality any longer. +* Methods unfold_locales and intro_locales ignore non-locale subgoals. This +is more appropriate for interpretations with 'where'. INCOMPATIBILITY. *** HOL ***