author | haftmann |
Thu, 04 Oct 2007 19:41:55 +0200 | |
changeset 24841 | df8448bc7a8b |
parent 24742 | 73b8b42a36b6 |
child 25517 | 36d710d1dbce |
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 |
|
20591 | 7 |
header {* A Basis for Building the Theory of Lists *} |
12020 | 8 |
|
15131 | 9 |
theory PreList |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24699
diff
changeset
|
10 |
imports ATP_Linkup |
24616 | 11 |
uses "Tools/function_package/lexicographic_order.ML" |
12 |
"Tools/function_package/fundef_datatype.ML" |
|
15131 | 13 |
begin |
12397 | 14 |
|
14577 | 15 |
text {* |
20591 | 16 |
This is defined separately to serve as a basis for |
17 |
theory ToyList in the documentation. |
|
18 |
*} |
|
14577 | 19 |
|
24616 | 20 |
(* The lexicographic_order method and the "fun" command *) |
21 |
setup LexicographicOrder.setup |
|
22 |
setup FundefDatatype.setup |
|
23 |
||
8490 | 24 |
end |