diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy --- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Fri Apr 04 23:12:20 2025 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Sat Apr 05 08:49:53 2025 +0200 @@ -5,7 +5,6 @@ theory Generate_Target_Bit_Operations imports "HOL-Library.Code_Test" - "HOL-Library.Code_Target_Bit_Shifts" begin context @@ -64,7 +63,7 @@ qualified definition \check_max = ()\ -qualified definition \anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\ +qualified definition \anchor = (Code_Numeral.drop_bit, check_max)\ end