NEWS
changeset 22799 ed7d53db2170
parent 22754 9947ae4792a0
child 22826 0f4c501a691e
     1.1 --- a/NEWS	Thu Apr 26 13:32:55 2007 +0200
     1.2 +++ b/NEWS	Thu Apr 26 13:32:59 2007 +0200
     1.3 @@ -515,6 +515,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
     1.8 +    when generating code.
     1.9 +
    1.10 +* Library/Pretty_Char.thy: maps HOL characters on target language character literals
    1.11 +    when generating code.
    1.12 +
    1.13  * Library/Commutative_Ring.thy: switched from recdef to function package;
    1.14      constants add, mul, pow now curried.  Infix syntax for algebraic operations.
    1.15