diff -r a1421c88ae0a -r 34cd1d210b92 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Fri Jul 01 20:47:16 2022 +0200 +++ b/src/Doc/Codegen/Adaptation.thy Mon Jul 04 07:57:22 2022 +0000 @@ -208,6 +208,10 @@ containing both \Code_Target_Nat\ and \Code_Target_Int\. + \item[\Code_Abstract_Char\] implements type \<^typ>\char\ by target language + integers, sacrificing pattern patching in exchange for dramatically + increased performance for comparisions. + \item[\<^theory>\HOL-Library.IArray\] provides a type \<^typ>\'a iarray\ isomorphic to lists but implemented by (effectively immutable) arrays \emph{in SML only}.