| changeset 50666 | 6f48853f08d5 |
| parent 50662 | b1f4291eb916 |
| child 54489 | 03ff4d1e6784 |
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Wed Jan 02 09:13:50 2013 +0100 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Wed Jan 02 09:31:25 2013 +0100 @@ -8,16 +8,8 @@ imports Complex_Main begin -declare [[smt_oracle = false]] -declare [[smt_certificates = "SMT_Tests.certs"]] -declare [[smt_read_only_certificates = true]] - - - smt_status - - text {* Most examples are taken from various Isabelle theories and from HOL4. *}