author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 9619 | 6125cc9efc18 |
child 10261 | bb2f1e859177 |
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 = |
|
10212 | 11 |
Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |
12 |
Relation_Power + Calculation + SVC_Oracle + While: |
|
8490 | 13 |
|
9066 | 14 |
theorems [cases type: bool] = case_split |
15 |
||
8490 | 16 |
end |