equal
deleted
inserted
replaced
40 |
40 |
41 * (Co)datatype package: |
41 * (Co)datatype package: |
42 - New commands for defining corecursive functions and reasoning about |
42 - New commands for defining corecursive functions and reasoning about |
43 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
43 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
44 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
44 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
45 method. |
45 method. See 'isabelle doc corec'. |
46 - The predicator :: ('a => bool) => 'a F => bool is now a first-class |
46 - The predicator :: ('a => bool) => 'a F => bool is now a first-class |
47 citizen in bounded natural functors |
47 citizen in bounded natural functors |
48 - 'primrec' now allows nested calls through the predicator in addition |
48 - 'primrec' now allows nested calls through the predicator in addition |
49 to the map function. |
49 to the map function. |
50 - 'bnf' automatically discharges reflexive proof obligations |
50 - 'bnf' automatically discharges reflexive proof obligations |