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