diff -r 29800666e526 -r 842917225d56 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/FSet.thy Tue Feb 23 16:25:08 2016 +0100 @@ -300,8 +300,8 @@ 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]