diff -r e77e8ef5bf9b -r 0ca0a47235e5 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Mon Dec 23 21:22:10 2024 +0100 +++ b/src/HOL/Code_Numeral.thy Mon Dec 23 21:58:26 2024 +0100 @@ -872,6 +872,26 @@ 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