# HG changeset patch
# User desharna
# Date 1632926947 -7200
# Node ID 162e63564e5aa7b208d9a417e01f3b0b50d8ef55
# Parent  776b74a9944930b2295f5392bfccf1d4dae69560# Parent  b9331caf92c3346d42802028c70aa155cdebca9b
merged

diff -r 776b74a99449 -r 162e63564e5a NEWS
--- a/NEWS	Tue Sep 28 17:14:21 2021 +0200
+++ b/NEWS	Wed Sep 29 16:49:07 2021 +0200
@@ -298,11 +298,11 @@
 
   val natT = \<^Type>\<open>nat\<close>;
   fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>;
-  val dest_funT = fn \<^Type>\<open>fun A B\<close> => (A, B);
+  val dest_funT = \<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>;
   fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>;
-  val dest_conj = fn \<^Const_>\<open>conj for A B\<close> => (A, B);
+  val dest_conj = \<^Const_fn>\<open>conj for A B => \<open>(A, B)\<close>\<close>;
   fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
-  val dest_eq = fn \<^Const_>\<open>HOL.eq T for t u\<close> => (T, (t, u));
+  val dest_eq = \<^Const_fn>\<open>HOL.eq T for t u => \<open>(T, (t, u))\<close>\<close>;
 
 * The "build" combinators of various data structures help to build
 content from bottom-up, by applying an "add" function the "empty" value.
diff -r 776b74a99449 -r 162e63564e5a src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Tue Sep 28 17:14:21 2021 +0200
+++ b/src/HOL/Bit_Operations.thy	Wed Sep 29 16:49:07 2021 +0200
@@ -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 776b74a99449 -r 162e63564e5a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Sep 28 17:14:21 2021 +0200
+++ b/src/HOL/Library/Word.thy	Wed Sep 29 16:49:07 2021 +0200
@@ -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 776b74a99449 -r 162e63564e5a src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Tue Sep 28 17:14:21 2021 +0200
+++ b/src/HOL/SPARK/SPARK.thy	Wed Sep 29 16:49:07 2021 +0200
@@ -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)