# HG changeset patch
# User nipkow
# Date 953884608 -3600
# Node ID 2746bc9a7ef266aa672f574797e3329469084d84
# Parent  ce0e2b8e88446576d4c7d57c67a80d0dc0593cf1
comments

diff -r ce0e2b8e8844 -r 2746bc9a7ef2 src/HOL/PreList.thy
--- 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