| changeset 52637 | 1501ebe39711 |
| parent 52550 | 09e52d4a850a |
| child 52653 | 0589394aaaa5 |
--- a/NEWS Sat Jul 13 17:53:57 2013 +0200 +++ b/NEWS Sat Jul 13 17:53:58 2013 +0200 @@ -84,6 +84,9 @@ *** HOL *** +* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly. +Use explicit 'code equation' and 'code abstract' to distinguish both when desired. + * Code generator: * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'. * 'code_identifier' declares name hints for arbitrary identifiers in generated code,