diff -r d80b2df54d31 -r a96320074298 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/SAT.thy Sun Jan 06 15:04:34 2019 +0100 @@ -11,10 +11,10 @@ imports Argo begin -ML_file "Tools/prop_logic.ML" -ML_file "Tools/sat_solver.ML" -ML_file "Tools/sat.ML" -ML_file "Tools/Argo/argo_sat_solver.ML" +ML_file \Tools/prop_logic.ML\ +ML_file \Tools/sat_solver.ML\ +ML_file \Tools/sat.ML\ +ML_file \Tools/Argo/argo_sat_solver.ML\ method_setup sat = \Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\ "SAT solver"