src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 63507 79122bdd4404
parent 62549 9498623b27f0
child 63518 ae8fd6fe63a1
equal deleted inserted replaced
63506:cb0882cf150d 63507:79122bdd4404
    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) =