290 rel_pow_finite_bounded ~> relpow_finite_bounded |
290 rel_pow_finite_bounded ~> relpow_finite_bounded |
291 rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow |
291 rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow |
292 trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow |
292 trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow |
293 single_valued_rel_pow ~> single_valued_relpow |
293 single_valued_rel_pow ~> single_valued_relpow |
294 |
294 |
|
295 INCOMPATIBILITY. |
|
296 |
|
297 * Theory Relation: Consolidated constant name for relation composition |
|
298 and corresponding theorem names: |
|
299 - Renamed constant rel_comp to relcomp |
|
300 - Dropped abbreviation pred_comp. Use relcompp instead. |
|
301 - Renamed theorems: |
|
302 Relation: |
|
303 rel_compI ~> relcompI |
|
304 rel_compEpair ~> relcompEpair |
|
305 rel_compE ~> relcompE |
|
306 pred_comp_rel_comp_eq ~> relcompp_relcomp_eq |
|
307 rel_comp_empty1 ~> relcomp_empty1 |
|
308 rel_comp_mono ~> relcomp_mono |
|
309 rel_comp_subset_Sigma ~> relcomp_subset_Sigma |
|
310 rel_comp_distrib ~> relcomp_distrib |
|
311 rel_comp_distrib2 ~> relcomp_distrib2 |
|
312 rel_comp_UNION_distrib ~> relcomp_UNION_distrib |
|
313 rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2 |
|
314 single_valued_rel_comp ~> single_valued_relcomp |
|
315 rel_comp_unfold ~> relcomp_unfold |
|
316 converse_rel_comp ~> converse_relcomp |
|
317 pred_compI ~> relcomppI |
|
318 pred_compE ~> relcomppE |
|
319 pred_comp_bot1 ~> relcompp_bot1 |
|
320 pred_comp_bot2 ~> relcompp_bot2 |
|
321 transp_pred_comp_less_eq ~> transp_relcompp_less_eq |
|
322 pred_comp_mono ~> relcompp_mono |
|
323 pred_comp_distrib ~> relcompp_distrib |
|
324 pred_comp_distrib2 ~> relcompp_distrib2 |
|
325 converse_pred_comp ~> converse_relcompp |
|
326 Transitive_Closure: |
|
327 finite_rel_comp ~> finite_relcomp |
|
328 List: |
|
329 set_rel_comp ~> set_relcomp |
|
330 |
295 INCOMPATIBILITY. |
331 INCOMPATIBILITY. |
296 |
332 |
297 * New theory HOL/Library/DAList provides an abstract type for association |
333 * New theory HOL/Library/DAList provides an abstract type for association |
298 lists with distinct keys. |
334 lists with distinct keys. |
299 |
335 |