src/HOL/PreList.thy
changeset 21457 84a21cf15923
parent 21330 6dd5919e7742
child 22844 91c05f4b509e
--- a/src/HOL/PreList.thy	Wed Nov 22 10:20:16 2006 +0100
+++ b/src/HOL/PreList.thy	Wed Nov 22 10:20:17 2006 +0100
@@ -8,7 +8,7 @@
 
 theory PreList
 imports Wellfounded_Relations Presburger Relation_Power SAT
-  Hilbert_Choice FunDef Extraction
+  FunDef Extraction
 begin
 
 text {*