equal
deleted
inserted
replaced
6 |
6 |
7 header {* A Basis for Building the Theory of Lists *} |
7 header {* A Basis for Building the Theory of Lists *} |
8 |
8 |
9 theory PreList |
9 theory PreList |
10 imports Presburger Relation_Power SAT Recdef Extraction Record |
10 imports Presburger Relation_Power SAT Recdef Extraction Record |
|
11 uses "Tools/function_package/lexicographic_order.ML" |
|
12 "Tools/function_package/fundef_datatype.ML" |
11 begin |
13 begin |
12 |
14 |
13 text {* |
15 text {* |
14 This is defined separately to serve as a basis for |
16 This is defined separately to serve as a basis for |
15 theory ToyList in the documentation. |
17 theory ToyList in the documentation. |
16 *} |
18 *} |
17 |
19 |
|
20 (* The lexicographic_order method and the "fun" command *) |
|
21 setup LexicographicOrder.setup |
|
22 setup FundefDatatype.setup |
|
23 |
18 end |
24 end |
19 |
25 |