changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 72508 | c89d8e8bd8c7 |
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Fri Aug 18 20:47:47 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Word examples for for SMT binding\<close> theory SMT_Word_Examples -imports "~~/src/HOL/Word/Word" +imports "HOL-Word.Word" begin declare [[smt_oracle = true]]