src/HOL/Library/FSet.thy

 lemmas fimage_funion = image_Un[Transfer.transferred]
 lemmas fimage_iff = image_iff[Transfer.transferred]
 lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
 lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred]
 lemmas fimage_ident[simp] = image_ident[Transfer.transferred]
-lemmas split_if_fmem1 = split_if_mem1[Transfer.transferred]
-lemmas split_if_fmem2 = split_if_mem2[Transfer.transferred]
+lemmas if_split_fmem1 = if_split_mem1[Transfer.transferred]
+lemmas if_split_fmem2 = if_split_mem2[Transfer.transferred]
 lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
 lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
 lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]
 lemmas pfsubset_eq = psubset_eq[Transfer.transferred]
 lemmas pfsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred]