| author | wenzelm |
| Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) | |
| changeset 24850 | 0cfd722ab579 |
| parent 24742 | 73b8b42a36b6 |
| child 25517 | 36d710d1dbce |
| permissions | -rw-r--r-- |
| nipkow@10519 | 1 |
(* Title: HOL/PreList.thy |
| nipkow@8563 | 2 |
ID: $Id$ |
| wenzelm@10733 | 3 |
Author: Tobias Nipkow and Markus Wenzel |
| nipkow@8563 | 4 |
Copyright 2000 TU Muenchen |
| nipkow@8563 | 5 |
*) |
| wenzelm@8490 | 6 |
|
| haftmann@20591 | 7 |
header {* A Basis for Building the Theory of Lists *}
|
| wenzelm@12020 | 8 |
|
| nipkow@15131 | 9 |
theory PreList |
| paulson@24742 | 10 |
imports ATP_Linkup |
| nipkow@24616 | 11 |
uses "Tools/function_package/lexicographic_order.ML" |
| nipkow@24616 | 12 |
"Tools/function_package/fundef_datatype.ML" |
| nipkow@15131 | 13 |
begin |
| wenzelm@12397 | 14 |
|
| wenzelm@14577 | 15 |
text {*
|
| haftmann@20591 | 16 |
This is defined separately to serve as a basis for |
| haftmann@20591 | 17 |
theory ToyList in the documentation. |
| haftmann@20591 | 18 |
*} |
| wenzelm@14577 | 19 |
|
| nipkow@24616 | 20 |
(* The lexicographic_order method and the "fun" command *) |
| nipkow@24616 | 21 |
setup LexicographicOrder.setup |
| nipkow@24616 | 22 |
setup FundefDatatype.setup |
| nipkow@24616 | 23 |
|
| wenzelm@8490 | 24 |
end |