| changeset 8563 | 2746bc9a7ef2 |
| parent 8490 | 6e0f23304061 |
| child 8756 | b03a0b219139 |
| 8562:ce0e2b8e8844 | 8563:2746bc9a7ef2 |
|---|---|
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 *) |
|
1 |
9 |
2 theory PreList = |
10 theory PreList = |
3 Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation + SVC_Oracle: |
11 Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation |
12 + SVC_Oracle: |
|
4 |
13 |
5 end |
14 end |