Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 63518 ae8fd6fe63a1
parent 63507 79122bdd4404
child 69593 3dda49e08b9d 
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -60,7 +60,7 @@
 fun print_cert cert =
   Output.information
     ("To repeat this proof with a certificate use this command:\n" ^
-      Active.sendback_markup [Markup.padding_command]
+      Active.sendback_markup_command
         ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
 
 fun sos_tac ctxt NONE =
isabelle