author | paulson |
Fri, 21 Apr 2000 11:28:18 +0200 | |
changeset 8756 | b03a0b219139 |
parent 8563 | 2746bc9a7ef2 |
child 8840 | 18b76c137c41 |
permissions | -rw-r--r-- |
8563 | 1 |
(* Title: HOL/List.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 2000 TU Muenchen |
|
5 |
||
6 |
A basis for building theory List on. Is defined separately to serve as a |
|
7 |
basis for theory ToyList in the documentation. |
|
8 |
*) |
|
8490 | 9 |
|
10 |
theory PreList = |
|
8563 | 11 |
Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation |
8756 | 12 |
+ SVC_Oracle |
13 |
files "Integ/NatSimprocs.ML": |
|
8490 | 14 |
|
15 |
end |