diff -r d8661799afb2 -r c7038c397ae3 src/HOL/SMT_Examples/SMT_Word_Examples.thy --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Thu Oct 29 09:59:40 2020 +0000 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Thu Oct 29 10:03:03 2020 +0000 @@ -5,7 +5,7 @@ section \Word examples for for SMT binding\ theory SMT_Word_Examples -imports "HOL-Word.Word" +imports "HOL-Library.Word" begin declare [[smt_oracle = true]]