equal
deleted
inserted
replaced
20 * Command '\<proof>' is an alias for 'sorry', with different |
20 * Command '\<proof>' is an alias for 'sorry', with different |
21 typesetting. E.g. to produce proof holes in examples and documentation. |
21 typesetting. E.g. to produce proof holes in examples and documentation. |
22 |
22 |
23 |
23 |
24 *** HOL *** |
24 *** HOL *** |
|
25 |
|
26 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
|
27 has been removed for output. It is retained for input only, until it is |
|
28 eliminated altogether. |
25 |
29 |
26 * (Co)datatype package: |
30 * (Co)datatype package: |
27 - the predicator :: ('a => bool) => 'a F => bool is now a first-class |
31 - the predicator :: ('a => bool) => 'a F => bool is now a first-class |
28 citizen in bounded natural functors |
32 citizen in bounded natural functors |
29 - "primrec" now allows nested calls through the predicator in addition |
33 - "primrec" now allows nested calls through the predicator in addition |