# HG changeset patch
# User haftmann
# Date 1745160309 -7200
# Node ID 803b5d19c48c7f0069ae652bd78023477e8d33ec
# Parent  c49564b6eb0f57160223f94d0291ab1634fdaac0
notes on bit shift rewrites

diff -r c49564b6eb0f -r 803b5d19c48c src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Sun Apr 20 11:42:13 2025 +0200
+++ b/src/Doc/Codegen/Adaptation.thy	Sun Apr 20 16:45:09 2025 +0200
@@ -190,6 +190,16 @@
        
        Part of \<open>HOL-Main\<close>.
 
+    \item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close>
+       isomorphic to lists but implemented by (effectively immutable)
+       arrays \emph{in SML only}.
+
+  \end{description}
+
+  \noindent Using these adaptation setups the following extensions are provided:
+
+  \begin{description}
+
     \item[\<open>Code_Target_Int\<close>] implements type \<^typ>\<open>int\<close>
        by \<^typ>\<open>integer\<close> and thus by target-language built-in integers.
 
@@ -207,14 +217,14 @@
     \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
        containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
 
+    \item[\<open>Code_Bit_Shifts_for_Arithmetic\<close>] uses the preprocessor to
+       replace arithmetic operations on numeric types by target-language
+       built-in bit shifts whenever feasible.
+
     \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language
        integers, sacrificing pattern patching in exchange for dramatically
        increased performance for comparisons.
 
-    \item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close>
-       isomorphic to lists but implemented by (effectively immutable)
-       arrays \emph{in SML only}.
-
   \end{description}
 \<close>