--- a/src/HOL/Library/Tools/smt_word.ML Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Tools/smt_word.ML Sun Aug 01 10:20:34 2021 +0000
@@ -130,10 +130,10 @@
(\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
(\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
(\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
- (\<^term>\<open>NOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
- (\<^term>\<open>(AND) :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
- (\<^term>\<open>(OR) :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
- (\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
+ (\<^term>\<open>not :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
+ (\<^term>\<open>and :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
+ (\<^term>\<open>or :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
+ (\<^term>\<open>xor :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
(\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
fold (add_word_fun shift) [
(\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),