# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1397949905 -3600
# Node ID 54505623a8efb3a155ec57742f5a88b2e7a8746d
# Parent  7eed0fee0241c53d733dea503de6718da974287f
sos accepts False, returns apply command

diff -r 7eed0fee0241 -r 54505623a8ef src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Apr 19 20:01:26 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sun Apr 20 00:25:05 2014 +0100
@@ -129,8 +129,8 @@
 (* certificate output *)
 
 fun output_line cert =
-  "To repeat this proof with a certifiate use this command:\n" ^
-    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
+  "To repeat this proof with a certificate use this command:\n" ^
+    Active.sendback_markup [] ("apply (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
 
diff -r 7eed0fee0241 -r 54505623a8ef src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Apr 19 20:01:26 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Apr 20 00:25:05 2014 +0100
@@ -961,7 +961,7 @@
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
+   @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},