# HG changeset patch
# User wenzelm
# Date 1655847376 -7200
# Node ID 29654a8e937472007015f24223e693db47429ddc
# Parent  d32201f08e98721aa8fbceafe285d25c56ee4d7d# Parent  5c1c4f537ae80f87250554f4a1ab0e6f1c3277fd
merged

diff -r 5c1c4f537ae8 -r 29654a8e9374 NEWS
--- a/NEWS	Tue Jun 21 23:30:19 2022 +0200
+++ b/NEWS	Tue Jun 21 23:36:16 2022 +0200
@@ -94,6 +94,9 @@
       image_mset_filter_mset_swap
       multp_image_mset_image_msetD
 
+* Theory "HOL-Library.Sublist":
+  - Added lemma map_mono_strict_suffix.
+
 * Sledgehammer:
   - Redesigned multithreading to provide more fine grained prover schedules.
     The binary option 'slice' has been replaced by a numeric value 'slices'
diff -r 5c1c4f537ae8 -r 29654a8e9374 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Tue Jun 21 23:30:19 2022 +0200
+++ b/src/HOL/Library/Sublist.thy	Tue Jun 21 23:36:16 2022 +0200
@@ -609,6 +609,9 @@
 lemma map_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (map f xs) (map f ys)"
 by (auto elim!: suffixE intro: suffixI)
 
+lemma map_mono_strict_suffix: "strict_suffix xs ys \<Longrightarrow> strict_suffix (map f xs) (map f ys)"
+  by (auto simp: strict_suffix_def suffix_def)
+
 lemma filter_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (filter P xs) (filter P ys)"
 by (auto simp: suffix_def)
 
diff -r 5c1c4f537ae8 -r 29654a8e9374 src/Pure/General/bytes.ML