Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Codegen/Adaptation.thy
changeset 82445 bb1f2a03b370
parent 81713 378b9d6c52b2 
--- 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>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated
        by a preprocessor.
 
-    \item[\<open>Code_Target_Bit_Shifts\<close>] implements bit shifts on \<^typ>\<open>integer\<close>
-       by target-language operations. Combined with \<open>Code_Target_Int\<close>
-       or \<open>Code_Target_Nat\<close>, bit shifts on \<^typ>\<open>int\<close> or \<^type>\<open>nat\<close> can
-       be implemented by target-language operations.
-
     \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>-
isabelle