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.