equal
deleted
inserted
replaced
10 theory Nat |
10 theory Nat |
11 imports Inductive Typedef Fun Fields |
11 imports Inductive Typedef Fun Fields |
12 begin |
12 begin |
13 |
13 |
14 ML_file "~~/src/Tools/rat.ML" |
14 ML_file "~~/src/Tools/rat.ML" |
|
15 |
|
16 named_theorems arith "arith facts -- only ground formulas" |
15 ML_file "Tools/arith_data.ML" |
17 ML_file "Tools/arith_data.ML" |
16 ML_file "~~/src/Provers/Arith/fast_lin_arith.ML" |
18 ML_file "~~/src/Provers/Arith/fast_lin_arith.ML" |
17 |
19 |
18 |
20 |
19 subsection {* Type @{text ind} *} |
21 subsection {* Type @{text ind} *} |