diff -r 7a9164068583 -r bb1f2a03b370 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Fri Apr 04 23:12:20 2025 +0200 +++ b/src/Doc/Codegen/Adaptation.thy Sat Apr 05 08:49:53 2025 +0200 @@ -204,11 +204,6 @@ Pattern matching with \<^term>\0::nat\ / \<^const>\Suc\ is eliminated by a preprocessor. - \item[\Code_Target_Bit_Shifts\] implements bit shifts on \<^typ>\integer\ - by target-language operations. Combined with \Code_Target_Int\ - or \Code_Target_Nat\, bit shifts on \<^typ>\int\ or \<^type>\nat\ can - be implemented by target-language operations. - \item[\Code_Target_Numeral\] is a convenience theory containing \Code_Target_Nat\, \Code_Target_Int\ and \Code_Target_Bit_Shifts\-