src/HOL/Real.thy

   zero_real_inst.zero_real
 
 
 subsection \<open>Setup for SMT\<close>
 
-ML_file "Tools/SMT/smt_real.ML"
-ML_file "Tools/SMT/z3_real.ML"
+ML_file \<open>Tools/SMT/smt_real.ML\<close>
+ML_file \<open>Tools/SMT/z3_real.ML\<close>
 
 lemma [z3_rule]:
   "0 + x = x"
   "x + 0 = x"
   "0 * x = 0"

   by auto
 
 
 subsection \<open>Setup for Argo\<close>
 
-ML_file "Tools/Argo/argo_real.ML"
+ML_file \<open>Tools/Argo/argo_real.ML\<close>
 
 end