src/HOL/PreList.thy
changeset 23708 b5eb0b4dd17d
parent 23465 8f8835aac299
child 24616 fac3dd4ade83
     1.1 --- a/src/HOL/PreList.thy	Tue Jul 10 17:30:47 2007 +0200
     1.2 +++ b/src/HOL/PreList.thy	Tue Jul 10 17:30:49 2007 +0200
     1.3 @@ -7,8 +7,7 @@
     1.4  header {* A Basis for Building the Theory of Lists *}
     1.5  
     1.6  theory PreList
     1.7 -imports Wellfounded_Relations Presburger Relation_Power SAT
     1.8 -  FunDef Recdef Extraction
     1.9 +imports Presburger Relation_Power SAT Recdef Extraction Record
    1.10  begin
    1.11  
    1.12  text {*
    1.13 @@ -17,3 +16,4 @@
    1.14  *}
    1.15  
    1.16  end
    1.17 +