# HG changeset patch
# User haftmann
# Date 1632898599 0
# Node ID 930047942f468df22ed0c1016ae21d440d9000ec
# Parent  23db3493478fb1cb429a808c1e2179417e60d263
repaired slip

diff -r 23db3493478f -r 930047942f46 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Sep 29 09:58:19 2021 +0200
+++ b/src/HOL/Bit_Operations.thy	Wed Sep 29 06:56:39 2021 +0000
@@ -3509,7 +3509,7 @@
 \<close>
 
 no_notation
-  not  (\<open>NOT"\<close>)
+  not  (\<open>NOT\<close>)
     and "and"  (infixr \<open>AND\<close> 64)
     and or  (infixr \<open>OR\<close>  59)
     and xor  (infixr \<open>XOR\<close> 59)
@@ -3518,7 +3518,7 @@
 begin
 
 notation
-  not  (\<open>NOT"\<close>)
+  not  (\<open>NOT\<close>)
     and "and"  (infixr \<open>AND\<close> 64)
     and or  (infixr \<open>OR\<close>  59)
     and xor  (infixr \<open>XOR\<close> 59)
diff -r 23db3493478f -r 930047942f46 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Sep 29 09:58:19 2021 +0200
+++ b/src/HOL/Library/Word.thy	Wed Sep 29 06:56:39 2021 +0000
@@ -1014,15 +1014,15 @@
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
   by (fact push_bit_of_1)
 
+context
+  includes bit_operations_syntax
+begin
+
 lemma [code]:
   \<open>NOT w = Word.of_int (NOT (Word.the_int w))\<close>
   for w :: \<open>'a::len word\<close>
   by transfer (simp add: take_bit_not_take_bit) 
 
-context
-  includes bit_operations_syntax
-begin
-
 lemma [code]:
   \<open>Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\<close>
   by transfer simp
@@ -1244,16 +1244,16 @@
   by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
     (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
 
+context
+  includes bit_operations_syntax
+begin
+
 lemma signed_not_eq:
   \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
   for w :: \<open>'b::len word\<close>
   by (simp add: bit_eq_iff bit_simps possible_bit_min possible_bit_less_imp min_less_iff_disj)
     (auto simp: min_def)
 
-context
-  includes bit_operations_syntax
-begin
-
 lemma signed_and_eq:
   \<open>signed (v AND w) = signed v AND signed w\<close>
   for v w :: \<open>'b::len word\<close>
diff -r 23db3493478f -r 930047942f46 src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Wed Sep 29 09:58:19 2021 +0200
+++ b/src/HOL/SPARK/SPARK.thy	Wed Sep 29 06:56:39 2021 +0000
@@ -37,7 +37,7 @@
   XOR_upper [of _ 64, simplified]
 
 lemma bit_not_spark_eq:
-  "NOT (word_of_int x :: ('a::len) word) =
+  "Bit_Operations.not (word_of_int x :: ('a::len) word) =
   word_of_int (2 ^ LENGTH('a) - 1 - x)"
   by (simp flip: mask_eq_exp_minus_1 add: of_int_mask_eq not_eq_complement)