author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 17508 | c84af7f39a6b |
child 20591 | 7cbb224598b2 |
permissions | -rw-r--r-- |
10519 | 1 |
(* Title: HOL/PreList.thy |
8563 | 2 |
ID: $Id$ |
10733 | 3 |
Author: Tobias Nipkow and Markus Wenzel |
8563 | 4 |
Copyright 2000 TU Muenchen |
5 |
*) |
|
8490 | 6 |
|
14125 | 7 |
header{*A Basis for Building the Theory of Lists*} |
12020 | 8 |
|
15131 | 9 |
theory PreList |
17508 | 10 |
imports Wellfounded_Relations Presburger Relation_Power Binomial |
15131 | 11 |
begin |
12397 | 12 |
|
14577 | 13 |
text {* |
14 |
Is defined separately to serve as a basis for theory ToyList in the |
|
15 |
documentation. *} |
|
16 |
||
8490 | 17 |
end |