NEWS
changeset 41031 9883d1417ce1
parent 41030 ff7d177128ef
child 41035 22a57175df20
equal deleted inserted replaced
41030:ff7d177128ef 41031:9883d1417ce1
   524   unique_lub      ~> is_lub_unique
   524   unique_lub      ~> is_lub_unique
   525   is_ub_lub       ~> is_lub_rangeD1
   525   is_ub_lub       ~> is_lub_rangeD1
   526   lub_bin_chain   ~> is_lub_bin_chain
   526   lub_bin_chain   ~> is_lub_bin_chain
   527   lub_fun         ~> is_lub_fun
   527   lub_fun         ~> is_lub_fun
   528   thelub_fun      ~> lub_fun
   528   thelub_fun      ~> lub_fun
       
   529   thelub_cfun     ~> lub_cfun
   529   thelub_Pair     ~> lub_Pair
   530   thelub_Pair     ~> lub_Pair
   530   lub_cprod       ~> is_lub_prod
   531   lub_cprod       ~> is_lub_prod
   531   thelub_cprod    ~> lub_prod
   532   thelub_cprod    ~> lub_prod
   532   minimal_cprod   ~> minimal_prod
   533   minimal_cprod   ~> minimal_prod
   533   inst_cprod_pcpo ~> inst_prod_pcpo
   534   inst_cprod_pcpo ~> inst_prod_pcpo