# HG changeset patch
# User haftmann
# Date 1574414701 0
# Node ID a7d1fb0c9e162101b999144732904c605be5876c
# Parent  9d2716dc79a6cd41f2582ab26a928e1a4f8d2674
proper prefix syntax

diff -r 9d2716dc79a6 -r a7d1fb0c9e16 NEWS
--- a/NEWS	Fri Nov 22 09:24:54 2019 +0000
+++ b/NEWS	Fri Nov 22 09:25:01 2019 +0000
@@ -87,6 +87,9 @@
 procedure for simple linear statements in metric spaces.
 
 
+* Word: Bitwise NOT-operator has proper prefix syntax.  Minor
+INCOMPATIBILITY.
+
 *** ML ***
 
 * Theory construction may be forked internally, the operation
diff -r 9d2716dc79a6 -r a7d1fb0c9e16 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Fri Nov 22 09:24:54 2019 +0000
+++ b/src/HOL/Word/Bits.thy	Fri Nov 22 09:25:01 2019 +0000
@@ -9,7 +9,7 @@
 begin
 
 class bit_operations =
-  fixes bitNOT :: "'a \<Rightarrow> 'a"  ("NOT _" [70] 71)
+  fixes bitNOT :: "'a \<Rightarrow> 'a"  ("NOT")
     and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
     and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
     and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
diff -r 9d2716dc79a6 -r a7d1fb0c9e16 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Nov 22 09:24:54 2019 +0000
+++ b/src/HOL/Word/Word.thy	Fri Nov 22 09:25:01 2019 +0000
@@ -2116,7 +2116,7 @@
   word_and_def word_or_def word_xor_def
 
 lemma word_wi_log_defs:
-  "NOT word_of_int a = word_of_int (NOT a)"
+  "NOT (word_of_int a) = word_of_int (NOT a)"
   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
@@ -2285,7 +2285,7 @@
   for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
-lemma word_not_not [simp]: "NOT NOT x = x"
+lemma word_not_not [simp]: "NOT (NOT x) = x"
   for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
@@ -4119,8 +4119,8 @@
 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
 
 lemma word_rot_logs:
-  "word_rotl n (NOT v) = NOT word_rotl n v"
-  "word_rotr n (NOT v) = NOT word_rotr n v"
+  "word_rotl n (NOT v) = NOT (word_rotl n v)"
+  "word_rotr n (NOT v) = NOT (word_rotr n v)"
   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"