src/HOL/Decision_Procs/Dense_Linear_Order.thy

 
 header {* Dense linear order without endpoints
   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
-imports Plain Groebner_Basis Main
+imports Main
 uses
   "~~/src/HOL/Tools/Qelim/langford_data.ML"
   "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
   ("~~/src/HOL/Tools/Qelim/langford.ML")
   ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML")