src/HOL/PreList.thy
changeset 21330 6dd5919e7742
parent 21256 47195501ecf7
child 21457 84a21cf15923
equal deleted inserted replaced
21329:7338206d75f1 21330:6dd5919e7742
     5 *)
     5 *)
     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
    10 imports Wellfounded_Relations Presburger Relation_Power SAT
       
    11   Hilbert_Choice FunDef Extraction
    11 begin
    12 begin
    12 
    13 
    13 text {*
    14 text {*
    14   This is defined separately to serve as a basis for
    15   This is defined separately to serve as a basis for
    15   theory ToyList in the documentation.
    16   theory ToyList in the documentation.