src/HOL/PreList.thy
author wenzelm
Mon May 08 20:59:30 2000 +0200 (2000-05-08)
changeset 8840 18b76c137c41
parent 8756 b03a0b219139
child 8862 78643f8449c6
permissions -rw-r--r--
moved theory Sexp to Induct examples;
nipkow@8563
     1
(*  Title:      HOL/List.thy
nipkow@8563
     2
    ID:         $Id$
nipkow@8563
     3
    Author:     Tobias Nipkow
nipkow@8563
     4
    Copyright   2000 TU Muenchen
nipkow@8563
     5
nipkow@8563
     6
A basis for building theory List on. Is defined separately to serve as a
nipkow@8563
     7
basis for theory ToyList in the documentation.
nipkow@8563
     8
*)
wenzelm@8490
     9
wenzelm@8490
    10
theory PreList =
wenzelm@8840
    11
  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
paulson@8756
    12
files "Integ/NatSimprocs.ML":
wenzelm@8490
    13
wenzelm@8490
    14
end