changeset 69605 | a96320074298 |
parent 67972 | 959b0aed2ce5 |
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy Sun Jan 06 15:04:34 2019 +0100 @@ -8,7 +8,7 @@ imports Complex_Main begin -external_file "SMT_Examples.certs" +external_file \<open>SMT_Examples.certs\<close> declare [[smt_certificates = "SMT_Examples.certs"]] declare [[smt_read_only_certificates = true]]