* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
authorwenzelm
Sat Oct 13 21:45:23 2001 +0200 (2001-10-13)
changeset 1174506cd8c3b5487
parent 11744 3a4625eaead0
child 11746 9bf11f1de9d6
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
NEWS
     1.1 --- a/NEWS	Sat Oct 13 21:44:58 2001 +0200
     1.2 +++ b/NEWS	Sat Oct 13 21:45:23 2001 +0200
     1.3 @@ -32,6 +32,8 @@
     1.4  
     1.5  * Pure: fixed 'token_translation' command;
     1.6  
     1.7 +* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
     1.8 +
     1.9  * HOL: 'recdef' now fails on unfinished automated proofs, use
    1.10  "(permissive)" option to recover old behavior;
    1.11