equal
deleted
inserted
replaced
437 use "Tools/Qelim/cooper.ML" |
437 use "Tools/Qelim/cooper.ML" |
438 oracle linzqe_oracle = Coopereif.cooper_oracle |
438 oracle linzqe_oracle = Coopereif.cooper_oracle |
439 |
439 |
440 use "Tools/Qelim/presburger.ML" |
440 use "Tools/Qelim/presburger.ML" |
441 |
441 |
442 declaration {* fn _ => |
442 setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *} |
443 arith_tactic_add |
|
444 (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st => |
|
445 (warning "Trying Presburger arithmetic ..."; |
|
446 Presburger.cooper_tac true [] [] ctxt i st))) |
|
447 *} |
|
448 |
443 |
449 method_setup presburger = {* |
444 method_setup presburger = {* |
450 let |
445 let |
451 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
446 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
452 fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () |
447 fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () |