
diff -r 3863850f4b0e -r 5dc2c98a6f16 src/HOL/Library/Code_Target_Bit_Shifts.thy
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 13:13:28 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 13:13:30 2025 +0100
@@ -101,7 +101,7 @@
 end;;
 \<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (Haskell) \<open>
-module Bit_Shifts where
+module Bit_Shifts (push, drop, push', drop') where
 
 import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip)
 import GHC.Bits (Bits)
@@ -123,17 +123,17 @@
 
 {- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -}
 
-push' :: Int -> Int -> Int
-push' i = flip shiftL (abs i)
-
 push :: Integer -> Integer -> Integer
 push i = fold (flip shiftL) (splitIndex (abs i))
 
+drop :: Integer -> Integer -> Integer
+drop i = fold (flip shiftR) (splitIndex (abs i))
+
+push' :: Int -> Int -> Int
+push' i = flip shiftL (abs i)
+
 drop' :: Int -> Int -> Int
 drop' i = flip shiftR (abs i)
-
-drop :: Integer -> Integer -> Integer
-drop i = fold (flip shiftR) (splitIndex (abs i))
 \<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (Scala) \<open>
 object Bit_Shifts {




