# HG changeset patch
# User haftmann
# Date 1163428987 -3600
# Node ID 6dd5919e77424f62786722a6c099bad7b85c672a
# Parent  7338206d75f163f775beaf5e8a369dbc99951636
PreList = Main - List

diff -r 7338206d75f1 -r 6dd5919e7742 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Mon Nov 13 15:43:06 2006 +0100
+++ b/src/HOL/PreList.thy	Mon Nov 13 15:43:07 2006 +0100
@@ -7,7 +7,8 @@
 header {* A Basis for Building the Theory of Lists *}
 
 theory PreList
-imports Wellfounded_Relations Presburger Relation_Power
+imports Wellfounded_Relations Presburger Relation_Power SAT
+  Hilbert_Choice FunDef Extraction
 begin
 
 text {*