1.1 --- a/src/HOL/PreList.thy	Thu Mar 23 21:37:13 2000 +0100
     1.2 +++ b/src/HOL/PreList.thy	Fri Mar 24 08:56:48 2000 +0100
     1.3 @@ -1,5 +1,14 @@
     1.4 +(*  Title:      HOL/List.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2000 TU Muenchen
     1.8 +
     1.9 +A basis for building theory List on. Is defined separately to serve as a
    1.10 +basis for theory ToyList in the documentation.
    1.11 +*)
    1.12  
    1.13  theory PreList =
    1.14 -  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation + SVC_Oracle:
    1.15 +  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
    1.16 +  + SVC_Oracle:
    1.17  
    1.18  end