diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Tue Oct 08 16:14:36 2024 +0200 +++ b/src/HOL/Bit_Operations.thy Tue Oct 08 16:15:31 2024 +0200 @@ -3986,21 +3986,15 @@ \bit (push_bit m k) n \ m \ n \ bit k (n - m)\ for k :: int by (fact bit_push_bit_iff') -no_notation - not (\NOT\) - and "and" (infixr \AND\ 64) - and or (infixr \OR\ 59) - and xor (infixr \XOR\ 59) - bundle bit_operations_syntax begin - notation not (\NOT\) and "and" (infixr \AND\ 64) and or (infixr \OR\ 59) and xor (infixr \XOR\ 59) +end + +unbundle no bit_operations_syntax end - -end