equal
deleted
inserted
replaced
384 One_nat_def,isolateSuc]; |
384 One_nat_def,isolateSuc]; |
385 |
385 |
386 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
386 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
387 (fn prems => [cut_facts_tac prems 1, |
387 (fn prems => [cut_facts_tac prems 1, |
388 blast_tac (claset() addIs [add_mono]) 1])) |
388 blast_tac (claset() addIs [add_mono]) 1])) |
389 ["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", |
389 ["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)", |
390 "(i = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", |
390 "(i = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)", |
391 "(i <= j) & (k = l) ==> i + k <= j + (l::'a::ordered_semiring)", |
391 "(i <= j) & (k = l) ==> i + k <= j + (l::'a::ordered_semidom)", |
392 "(i = j) & (k = l) ==> i + k = j + (l::'a::ordered_semiring)" |
392 "(i = j) & (k = l) ==> i + k = j + (l::'a::ordered_semidom)" |
393 ]; |
393 ]; |
394 |
394 |
395 in |
395 in |
396 |
396 |
397 val init_lin_arith_data = |
397 val init_lin_arith_data = |