324 - New commands for defining corecursive functions and reasoning about |
324 - New commands for defining corecursive functions and reasoning about |
325 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
325 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
326 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
326 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
327 method. See 'isabelle doc corec'. |
327 method. See 'isabelle doc corec'. |
328 - The predicator :: ('a => bool) => 'a F => bool is now a first-class |
328 - The predicator :: ('a => bool) => 'a F => bool is now a first-class |
329 citizen in bounded natural functors |
329 citizen in bounded natural functors. |
330 - 'primrec' now allows nested calls through the predicator in addition |
330 - 'primrec' now allows nested calls through the predicator in addition |
331 to the map function. |
331 to the map function. |
332 - 'bnf' automatically discharges reflexive proof obligations |
332 - 'bnf' automatically discharges reflexive proof obligations. |
333 - 'bnf' outputs a slightly modified proof obligation expressing rel in |
333 - 'bnf' outputs a slightly modified proof obligation expressing rel in |
334 terms of map and set |
334 terms of map and set |
335 (not giving a specification for rel makes this one reflexive) |
335 (not giving a specification for rel makes this one reflexive). |
336 - 'bnf' outputs a new proof obligation expressing pred in terms of set |
336 - 'bnf' outputs a new proof obligation expressing pred in terms of set |
337 (not giving a specification for pred makes this one reflexive) |
337 (not giving a specification for pred makes this one reflexive). |
338 INCOMPATIBILITY: manual 'bnf' declarations may need adjustment |
338 INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. |
339 - Renamed lemmas: |
339 - Renamed lemmas: |
340 rel_prod_apply ~> rel_prod_inject |
340 rel_prod_apply ~> rel_prod_inject |
341 pred_prod_apply ~> pred_prod_inject |
341 pred_prod_apply ~> pred_prod_inject |
342 INCOMPATIBILITY. |
342 INCOMPATIBILITY. |
343 - The "size" plugin has been made compatible again with locales. |
343 - The "size" plugin has been made compatible again with locales. |
|
344 - The theorems about "rel" and "set" may have a slightly different (but |
|
345 equivalent) form. |
|
346 INCOMPATIBILITY. |
344 |
347 |
345 * Some old / obsolete theorems have been renamed / removed, potential |
348 * Some old / obsolete theorems have been renamed / removed, potential |
346 INCOMPATIBILITY. |
349 INCOMPATIBILITY. |
347 |
350 |
348 nat_less_cases -- removed, use linorder_cases instead |
351 nat_less_cases -- removed, use linorder_cases instead |