NEWS
changeset 62693 0ae225877b68
parent 62678 843ff6f1de38
child 62789 ce15dd971965
equal deleted inserted replaced
62692:0701f25fac39 62693:0ae225877b68
    31 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
    31 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
    32 has been removed for output. It is retained for input only, until it is
    32 has been removed for output. It is retained for input only, until it is
    33 eliminated altogether.
    33 eliminated altogether.
    34 
    34 
    35 * (Co)datatype package:
    35 * (Co)datatype package:
    36   - the predicator :: ('a => bool) => 'a F => bool is now a first-class
    36   - New commands for defining corecursive functions and reasoning about
       
    37     them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
       
    38     'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
       
    39     method.
       
    40   - The predicator :: ('a => bool) => 'a F => bool is now a first-class
    37     citizen in bounded natural functors
    41     citizen in bounded natural functors
    38   - "primrec" now allows nested calls through the predicator in addition
    42   - 'primrec' now allows nested calls through the predicator in addition
    39     to the map function.
    43     to the map function.
    40   - "bnf" automatically discharges reflexive proof obligations
    44   - 'bnf' automatically discharges reflexive proof obligations
    41     "bnf" outputs a slightly modified proof obligation expressing rel in
    45   - 'bnf' outputs a slightly modified proof obligation expressing rel in
    42        terms of map and set
    46        terms of map and set
    43        (not giving a specification for rel makes this one reflexive)
    47        (not giving a specification for rel makes this one reflexive)
    44     "bnf" outputs a new proof obligation expressing pred in terms of set
    48   - 'bnf' outputs a new proof obligation expressing pred in terms of set
    45        (not giving a specification for pred makes this one reflexive)
    49        (not giving a specification for pred makes this one reflexive)
    46     INCOMPATIBILITY: manual "bnf" declarations may need adjustment
    50     INCOMPATIBILITY: manual 'bnf' declarations may need adjustment
    47   - Renamed lemmas:
    51   - Renamed lemmas:
    48       rel_prod_apply ~> rel_prod_inject
    52       rel_prod_apply ~> rel_prod_inject
    49       pred_prod_apply ~> pred_prod_inject
    53       pred_prod_apply ~> pred_prod_inject
    50     INCOMPATIBILITY.
    54     INCOMPATIBILITY.
    51   - The "size" plugin has been made compatible again with locales.
    55   - The "size" plugin has been made compatible again with locales.