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