diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/AList_Mapping.thy --- a/src/HOL/Library/AList_Mapping.thy Fri Jun 06 18:36:29 2025 +0100 +++ b/src/HOL/Library/AList_Mapping.thy Mon Jun 09 22:14:38 2025 +0200 @@ -22,7 +22,7 @@ by transfer simp lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \ List.null xs" - by (cases xs) (simp_all add: is_empty_def null_def) + by (cases xs) (simp_all add: is_empty_def) lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)" by transfer (simp add: update_conv')