diff -r 97987036f051 -r 378b9d6c52b2 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/Doc/Codegen/Adaptation.thy Sat Jan 04 14:41:30 2025 +0100 @@ -204,13 +204,17 @@ 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 both \Code_Target_Nat\ and - \Code_Target_Int\. + containing \Code_Target_Nat\, \Code_Target_Int\ and \Code_Target_Bit_Shifts\- \item[\Code_Abstract_Char\] implements type \<^typ>\char\ by target language integers, sacrificing pattern patching in exchange for dramatically - increased performance for comparisions. + increased performance for comparisons. \item[\<^theory>\HOL-Library.IArray\] provides a type \<^typ>\'a iarray\ isomorphic to lists but implemented by (effectively immutable)