# HG changeset patch # User wenzelm # Date 1632680008 -7200 # Node ID d1185d02aef5ca0ca86c05b6adfecbe4df837267 # Parent 99add5178e51519de89c36f31e87c557b6e87ac7# Parent b49bd5d9041f3cb6c5269e4645ed56d3b5aabd40 merged diff -r b49bd5d9041f -r d1185d02aef5 NEWS --- a/NEWS Sun Sep 26 18:49:55 2021 +0200 +++ b/NEWS Sun Sep 26 20:13:28 2021 +0200 @@ -214,7 +214,7 @@ * Combinator "Fun.swap" resolved into a mere input abbreviation in separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. -* Infix syntax for bit operations AND, OR, XOR is now organized in +* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in bundle bit_operations_syntax. INCOMPATIBILITY. * Bit operations set_bit, unset_bit and flip_bit are now class diff -r b49bd5d9041f -r d1185d02aef5 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Sun Sep 26 18:49:55 2021 +0200 +++ b/src/HOL/Bit_Operations.thy Sun Sep 26 20:13:28 2021 +0200 @@ -3509,7 +3509,8 @@ \ no_notation - "and" (infixr \AND\ 64) + not (\NOT"\) + and "and" (infixr \AND\ 64) and or (infixr \OR\ 59) and xor (infixr \XOR\ 59) @@ -3517,7 +3518,8 @@ begin notation - "and" (infixr \AND\ 64) + not (\NOT"\) + and "and" (infixr \AND\ 64) and or (infixr \OR\ 59) and xor (infixr \XOR\ 59)