equal
deleted
inserted
replaced
1334 using 2 1 by (rule trans) |
1334 using 2 1 by (rule trans) |
1335 |
1335 |
1336 use "Tools/arith_data.ML" |
1336 use "Tools/arith_data.ML" |
1337 declaration {* K ArithData.setup *} |
1337 declaration {* K ArithData.setup *} |
1338 |
1338 |
|
1339 ML{* |
|
1340 structure ArithFacts = |
|
1341 NamedThmsFun(val name = "arith" |
|
1342 val description = "arith facts - only ground formulas"); |
|
1343 *} |
|
1344 |
|
1345 setup ArithFacts.setup |
|
1346 |
1339 use "Tools/lin_arith.ML" |
1347 use "Tools/lin_arith.ML" |
1340 declaration {* K LinArith.setup *} |
1348 declaration {* K LinArith.setup *} |
1341 |
1349 |
1342 lemmas [arith_split] = nat_diff_split split_min split_max |
1350 lemmas [arith_split] = nat_diff_split split_min split_max |
1343 |
|
1344 |
1351 |
1345 context order |
1352 context order |
1346 begin |
1353 begin |
1347 |
1354 |
1348 lemma lift_Suc_mono_le: |
1355 lemma lift_Suc_mono_le: |