| changeset 35121 | 36c0a6dd8c6f |
| parent 35064 | 1bdef0c013d3 |
| child 35216 | 7641e8d831d2 |
| 35120:0a3adceb9c67 | 35121:36c0a6dd8c6f |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Natural numbers *} |
8 header {* Natural numbers *} |
9 |
9 |
10 theory Nat |
10 theory Nat |
11 imports Inductive Product_Type Fields |
11 imports Inductive Typedef Fun Fields |
12 uses |
12 uses |
13 "~~/src/Tools/rat.ML" |
13 "~~/src/Tools/rat.ML" |
14 "~~/src/Provers/Arith/cancel_sums.ML" |
14 "~~/src/Provers/Arith/cancel_sums.ML" |
15 "Tools/arith_data.ML" |
15 "Tools/arith_data.ML" |
16 ("Tools/nat_arith.ML") |
16 ("Tools/nat_arith.ML") |