--- a/src/HOL/PreList.thy Thu Mar 23 21:37:13 2000 +0100
+++ b/src/HOL/PreList.thy Fri Mar 24 08:56:48 2000 +0100
@@ -1,5 +1,14 @@
+(* Title: HOL/List.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TU Muenchen
+
+A basis for building theory List on. Is defined separately to serve as a
+basis for theory ToyList in the documentation.
+*)
theory PreList =
- Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation + SVC_Oracle:
+ Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
+ + SVC_Oracle:
end