442 - Infinite products of probability measures are now available. |
442 - Infinite products of probability measures are now available. |
443 - Sigma closure is independent, if the generator is independent |
443 - Sigma closure is independent, if the generator is independent |
444 - Use extended reals instead of positive extended |
444 - Use extended reals instead of positive extended |
445 reals. INCOMPATIBILITY. |
445 reals. INCOMPATIBILITY. |
446 |
446 |
|
447 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY. |
|
448 |
|
449 expand_fun_below ~> fun_below_iff |
|
450 below_fun_ext ~> fun_belowI |
|
451 expand_cfun_eq ~> cfun_eq_iff |
|
452 ext_cfun ~> cfun_eqI |
|
453 expand_cfun_below ~> cfun_below_iff |
|
454 below_cfun_ext ~> cfun_belowI |
|
455 monofun_fun_fun ~> fun_belowD |
|
456 monofun_fun_arg ~> monofunE |
|
457 monofun_lub_fun ~> adm_monofun [THEN admD] |
|
458 cont_lub_fun ~> adm_cont [THEN admD] |
|
459 cont2cont_Rep_CFun ~> cont2cont_APP |
|
460 cont_Rep_CFun_app ~> cont_APP_app |
|
461 cont_Rep_CFun_app_app ~> cont_APP_app_app |
|
462 cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE] |
|
463 cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE] |
|
464 contlub_cfun ~> lub_APP [symmetric] |
|
465 contlub_LAM ~> lub_LAM [symmetric] |
|
466 thelubI ~> lub_eqI |
|
467 UU_I ~> bottomI |
|
468 lift_distinct1 ~> lift.distinct(1) |
|
469 lift_distinct2 ~> lift.distinct(2) |
|
470 Def_not_UU ~> lift.distinct(2) |
|
471 Def_inject ~> lift.inject |
|
472 below_UU_iff ~> below_bottom_iff |
|
473 eq_UU_iff ~> eq_bottom_iff |
|
474 |
447 |
475 |
448 *** Document preparation *** |
476 *** Document preparation *** |
449 |
477 |
450 * Antiquotation @{rail} layouts railroad syntax diagrams, see also |
478 * Antiquotation @{rail} layouts railroad syntax diagrams, see also |
451 isar-ref manual, both for description and actual application of the |
479 isar-ref manual, both for description and actual application of the |