equal
deleted
inserted
replaced
14 |
14 |
15 |
15 |
16 *** HOL *** |
16 *** HOL *** |
17 |
17 |
18 * (Co)datatype package: |
18 * (Co)datatype package: |
|
19 - the predicator :: ('a => bool) => 'a F => bool is now a first-class |
|
20 citizen in bounded natural functors |
19 - "primrec" now allows nested calls through the predicator in addition |
21 - "primrec" now allows nested calls through the predicator in addition |
20 to the map function. |
22 to the map function. |
|
23 - "bnf" automatically discharges reflexive proof obligations |
|
24 "bnf" outputs a slightly modified proof obligation expressing rel in |
|
25 terms of map and set |
|
26 (not giving a specification for rel makes this one reflexive) |
|
27 "bnf" outputs a new proof obligation expressing pred in terms of set |
|
28 (not giving a specification for pred makes this one reflexive) |
|
29 INCOMPATIBILITY: manual "bnf" declarations may need adjustment |
21 |
30 |
22 |
31 |
23 New in Isabelle2016 (February 2016) |
32 New in Isabelle2016 (February 2016) |
24 ----------------------------------- |
33 ----------------------------------- |
25 |
34 |