src/HOL/Library/Code_Target_Bit_Shifts.thy

--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:56 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:57 2025 +0100
@@ -41,6 +41,7 @@
   type int = IntInf.int
   val push : int -> int -> int
   val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
 end = struct
 
 type int = IntInf.int;