src/HOL/PreList.thy
changeset 21457 84a21cf15923
parent 21330 6dd5919e7742
child 22844 91c05f4b509e
equal deleted inserted replaced
21456:1c2b9df41e98 21457:84a21cf15923
     6 
     6 
     7 header {* A Basis for Building the Theory of Lists *}
     7 header {* A Basis for Building the Theory of Lists *}
     8 
     8 
     9 theory PreList
     9 theory PreList
    10 imports Wellfounded_Relations Presburger Relation_Power SAT
    10 imports Wellfounded_Relations Presburger Relation_Power SAT
    11   Hilbert_Choice FunDef Extraction
    11   FunDef Extraction
    12 begin
    12 begin
    13 
    13 
    14 text {*
    14 text {*
    15   This is defined separately to serve as a basis for
    15   This is defined separately to serve as a basis for
    16   theory ToyList in the documentation.
    16   theory ToyList in the documentation.