diff -r 88feb0047d7c -r bac9b067c768 src/HOL/Code_Numeral.thy --- 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 \ integer \ integer" \ - (SML) "IntInf.andb ((_),/ (_))" - and (OCaml) "Z.logand" - and (Haskell) infixl 7 ".&." - and (Scala) infixl 3 "&" -| constant "Bit_Operations.or :: integer \ integer \ integer" \ - (SML) "IntInf.orb ((_),/ (_))" - and (OCaml) "Z.logor" - and (Haskell) infixl 5 ".|." - and (Scala) infixl 1 "|" -| constant "Bit_Operations.xor :: integer \ integer \ integer" \ - (SML) "IntInf.xorb ((_),/ (_))" - and (OCaml) "Z.logxor" - and (Haskell) infixl 6 ".^." - and (Scala) infixl 2 "^" -| constant "Bit_Operations.not :: integer \ integer" \ - (SML) "IntInf.notb" - and (OCaml) "Z.lognot" - and (Haskell) "Data.Bits.complement" - and (Scala) "_.unary'_~" code_identifier code_module Code_Numeral \ (SML) Arith and (OCaml) Arith and (Haskell) Arith