src/HOL/Dense_Linear_Order.thy

   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
 imports Finite_Set
 uses
-  "Tools/qelim.ML"
-  "Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML"
-  ("Tools/Ferrante_Rackoff/ferrante_rackoff.ML")
+  "Tools/Qelim/qelim.ML"
+  "Tools/Qelim/ferrante_rackoff_data.ML"
+  ("Tools/Qelim/ferrante_rackoff.ML")
 begin
 
 setup Ferrante_Rackoff_Data.setup
 
 context Linorder

 end
 *}
 
 end
 
-use "Tools/Ferrante_Rackoff/ferrante_rackoff.ML"
+use "Tools/Qelim/ferrante_rackoff.ML"
 
 method_setup dlo = {*
   Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"