equal
deleted
inserted
replaced
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 certifiate use this command:\n" ^ |
133 Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")") |
133 Markup.markup Isabelle_Markup.sendback ("by (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 *) |