* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

--- a/NEWS	Sat Oct 13 21:44:58 2001 +0200
+++ b/NEWS	Sat Oct 13 21:45:23 2001 +0200
@@ -32,6 +32,8 @@
 
 * Pure: fixed 'token_translation' command;
 
+* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
+
 * HOL: 'recdef' now fails on unfinished automated proofs, use
 "(permissive)" option to recover old behavior;