src/HOL/PreList.thy
changeset 13878 90ca3815e4b2
parent 13297 e4ae0732e2be
child 14125 bf8edef6c1f1
equal deleted inserted replaced
13877:a6b825ee48d9 13878:90ca3815e4b2
     6 A basis for building theory List on. Is defined separately to serve as a
     6 A basis for building theory List on. Is defined separately to serve as a
     7 basis for theory ToyList in the documentation.
     7 basis for theory ToyList in the documentation.
     8 *)
     8 *)
     9 
     9 
    10 theory PreList =
    10 theory PreList =
    11   Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power:
    11   Wellfounded_Relations + Presburger + Recdef + Relation_Power:
    12 
    12 
    13 (*belongs to theory Divides*)
    13 (*belongs to theory Divides*)
    14 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    14 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    15 
    15 
    16 (*belongs to theory Nat*)
    16 (*belongs to theory Nat*)