--- a/src/HOL/PreList.thy Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/PreList.thy Thu Sep 27 17:55:28 2007 +0200
@@ -7,7 +7,7 @@
header {* A Basis for Building the Theory of Lists *}
theory PreList
-imports Presburger Relation_Power SAT Recdef Extraction Record ATP_Linkup
+imports ATP_Linkup
uses "Tools/function_package/lexicographic_order.ML"
"Tools/function_package/fundef_datatype.ML"
begin
@@ -21,7 +21,4 @@
setup LexicographicOrder.setup
setup FundefDatatype.setup
-(*Sledgehammer*)
-setup ResAxioms.setup
-
end