src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 56625 54505623a8ef
parent 52697 6fb98a20c349
child 58418 a04b242a7a01
equal deleted inserted replaced
56624:7eed0fee0241 56625:54505623a8ef
   127 
   127 
   128 
   128 
   129 (* certificate output *)
   129 (* certificate output *)
   130 
   130 
   131 fun output_line cert =
   131 fun output_line cert =
   132   "To repeat this proof with a certifiate use this command:\n" ^
   132   "To repeat this proof with a certificate use this command:\n" ^
   133     Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
   133     Active.sendback_markup [] ("apply (sos_cert \"" ^ cert ^ "\")")
   134 
   134 
   135 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
   135 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
   136 
   136 
   137 
   137 
   138 (* method setup *)
   138 (* method setup *)