src/HOL/Code_Numeral.thy
changeset 81681 bac9b067c768
parent 81643 0ca0a47235e5
child 81706 7beb0cf38292
--- a/src/HOL/Code_Numeral.thy	Sat Dec 28 18:03:41 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Dec 28 21:20:33 2024 +0100
@@ -872,26 +872,6 @@
     and (Haskell) "Prelude.abs"
     and (Scala) "_.abs"
     and (Eval) "abs"
-| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.andb ((_),/ (_))"
-    and (OCaml) "Z.logand"
-    and (Haskell) infixl 7 ".&."
-    and (Scala) infixl 3 "&"
-| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.orb ((_),/ (_))"
-    and (OCaml) "Z.logor"
-    and (Haskell) infixl 5 ".|."
-    and (Scala) infixl 1 "|"
-| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.xorb ((_),/ (_))"
-    and (OCaml) "Z.logxor"
-    and (Haskell) infixl 6 ".^."
-    and (Scala) infixl 2 "^"
-| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.notb"
-    and (OCaml) "Z.lognot"
-    and (Haskell) "Data.Bits.complement"
-    and (Scala) "_.unary'_~"
 
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith