| changeset 63343 | fb5d8a50c641 |
| parent 63310 | caaacf37943f |
| child 63350 | 705229ed856e |
| child 63352 | 4eaf35781b23 |
--- a/NEWS Tue Jun 21 17:35:45 2016 +0200 +++ b/NEWS Wed Jun 22 10:09:20 2016 +0200 @@ -132,6 +132,10 @@ *** HOL *** +* Former locale lifting_syntax is now a bundle, which is easier to +include in a local context or theorem statement, e.g. "context includes +lifting_syntax begin ... end". Minor INCOMPATIBILITY. + * Code generation for scala: ambiguous implicts in class diagrams are spelt out explicitly.