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