nipkow@8563: (* Title: HOL/List.thy nipkow@8563: ID: $Id$ nipkow@8563: Author: Tobias Nipkow nipkow@8563: Copyright 2000 TU Muenchen nipkow@8563: nipkow@8563: A basis for building theory List on. Is defined separately to serve as a nipkow@8563: basis for theory ToyList in the documentation. nipkow@8563: *) wenzelm@8490: wenzelm@8490: theory PreList = nipkow@8563: Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation nipkow@8563: + SVC_Oracle: wenzelm@8490: wenzelm@8490: end