| changeset 11745 | 06cd8c3b5487 |
| parent 11738 | 7c7a902a5c65 |
| child 11788 | 60054fee3c16 |
--- 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;