src/HOL/PreList.thy
changeset 15131 c69542757a4d
parent 14577 dbb95b825244
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     4     Copyright   2000 TU Muenchen
     4     Copyright   2000 TU Muenchen
     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     Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
    10 import Wellfounded_Relations Presburger Recdef Relation_Power Parity
       
    11 begin
    11 
    12 
    12 text {*
    13 text {*
    13   Is defined separately to serve as a basis for theory ToyList in the
    14   Is defined separately to serve as a basis for theory ToyList in the
    14   documentation. *}
    15   documentation. *}
    15 
    16