changeset 21330 | 6dd5919e7742 |
parent 21256 | 47195501ecf7 |
child 21457 | 84a21cf15923 |
--- 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 {*