NEWS
changeset 62842 db9f95ca2a8f
parent 62840 d9744f41a4ec
child 62851 07eea2843b82
equal deleted inserted replaced
62841:388719339ada 62842:db9f95ca2a8f
    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