author | paulson |
Fri, 21 Apr 2000 11:28:18 +0200 | |
changeset 8756 | b03a0b219139 |
parent 8563 | 2746bc9a7ef2 |
child 8840 | 18b76c137c41 |
permissions | -rw-r--r-- |
(* 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 files "Integ/NatSimprocs.ML": end