--- 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)
--- 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>
--- 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)