equal
deleted
inserted
replaced
58 (* method setup *) |
58 (* method setup *) |
59 |
59 |
60 fun print_cert cert = |
60 fun print_cert cert = |
61 Output.information |
61 Output.information |
62 ("To repeat this proof with a certificate use this command:\n" ^ |
62 ("To repeat this proof with a certificate use this command:\n" ^ |
63 Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) |
63 Active.sendback_markup [Markup.padding_command] |
|
64 ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) |
64 |
65 |
65 fun sos_tac ctxt NONE = |
66 fun sos_tac ctxt NONE = |
66 Sum_of_Squares.sos_tac print_cert |
67 Sum_of_Squares.sos_tac print_cert |
67 (Sum_of_Squares.Prover (run_solver ctxt)) ctxt |
68 (Sum_of_Squares.Prover (run_solver ctxt)) ctxt |
68 | sos_tac ctxt (SOME cert) = |
69 | sos_tac ctxt (SOME cert) = |