| changeset 62521 | 6383440f41a8 |
| parent 62519 | a564458f94db |
| child 62522 | d32c23d29968 |
--- a/NEWS Sat Mar 05 19:14:04 2016 +0100 +++ b/NEWS Sat Mar 05 19:58:56 2016 +0100 @@ -23,6 +23,10 @@ *** HOL *** +* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" +has been removed for output. It is retained for input only, until it is +eliminated altogether. + * (Co)datatype package: - the predicator :: ('a => bool) => 'a F => bool is now a first-class citizen in bounded natural functors