| changeset 47152 | 446cfc760ccf |
| parent 47111 | a4476e55a241 |
| child 47155 | ade3fc826af3 |
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Mar 27 16:59:13 2012 +0300 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Mar 27 16:59:13 2012 +0300 @@ -8,9 +8,9 @@ imports Complex_Main begin -declare [[smt_oracle=false]] -declare [[smt_certificates="SMT_Tests.certs"]] -declare [[smt_fixed=true]] +declare [[smt_oracle = false]] +declare [[smt_certificates = "SMT_Tests.certs"]] +declare [[smt_read_only_certificates = true]]