src/HOL/SMT_Examples/SMT_Examples.thy
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]]