src/HOL/Decision_Procs/Dense_Linear_Order.thy

 
 theory Dense_Linear_Order
 imports Main
 begin
 
-ML_file "langford_data.ML"
-ML_file "ferrante_rackoff_data.ML"
+ML_file \<open>langford_data.ML\<close>
+ML_file \<open>ferrante_rackoff_data.ML\<close>
 
 context linorder
 begin
 
 lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)"

 lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))"
   by blast
 
 lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
 
-ML_file "langford.ML"
+ML_file \<open>langford.ML\<close>
 method_setup dlo = \<open>
   Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
 \<close> "Langford's algorithm for quantifier elimination in dense linear orders"
 
 

 end
 \<close>
 
 end
 
-ML_file "ferrante_rackoff.ML"
+ML_file \<open>ferrante_rackoff.ML\<close>
 
 method_setup ferrack = \<open>
   Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
 \<close> "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"