src/HOL/SMT_Examples/SMT_Word_Examples.thy

--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Aug 01 10:20:34 2021 +0000
@@ -35,6 +35,10 @@
 
 section \<open>Bit-level logic\<close>
 
+context
+  includes bit_operations_syntax
+begin
+
 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt
 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt
 lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt
@@ -52,6 +56,8 @@
 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
 lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
 
+end
+
 
 section \<open>Combined integer-bitvector properties\<close>