# HG changeset patch
# User wenzelm
# Date 1003002323 -7200
# Node ID 06cd8c3b5487b09452d7101a4061601e3d637255
# Parent  3a4625eaead099e66946857b480db5a9cb1f6bc7
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

diff -r 3a4625eaead0 -r 06cd8c3b5487 NEWS
--- 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;