| changeset 72515 | c7038c397ae3 |
| parent 72514 | d8661799afb2 |
| child 74097 | 6d7be1227d02 |
--- 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 \<open>Word examples for for SMT binding\<close> theory SMT_Word_Examples -imports "HOL-Word.Word" +imports "HOL-Library.Word" begin declare [[smt_oracle = true]]