equal
deleted
inserted
replaced
8 |
8 |
9 header {* Natural numbers *} |
9 header {* Natural numbers *} |
10 |
10 |
11 theory Nat |
11 theory Nat |
12 imports Wellfounded_Recursion Ring_and_Field |
12 imports Wellfounded_Recursion Ring_and_Field |
13 uses ("arith_data.ML") |
13 uses |
|
14 "~~/src/Tools/rat.ML" |
|
15 "~~/src/Provers/Arith/fast_lin_arith.ML" |
|
16 "~~/src/Provers/Arith/cancel_sums.ML" |
|
17 ("arith_data.ML") |
14 begin |
18 begin |
15 |
19 |
16 subsection {* Type @{text ind} *} |
20 subsection {* Type @{text ind} *} |
17 |
21 |
18 typedecl ind |
22 typedecl ind |