equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Word examples for for SMT binding\<close> |
5 section \<open>Word examples for for SMT binding\<close> |
6 |
6 |
7 theory SMT_Word_Examples |
7 theory SMT_Word_Examples |
8 imports "~~/src/HOL/Word/Word" |
8 imports "HOL-Word.Word" |
9 begin |
9 begin |
10 |
10 |
11 declare [[smt_oracle = true]] |
11 declare [[smt_oracle = true]] |
12 declare [[z3_extensions = true]] |
12 declare [[z3_extensions = true]] |
13 declare [[smt_certificates = "SMT_Word_Examples.certs"]] |
13 declare [[smt_certificates = "SMT_Word_Examples.certs"]] |