--- 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
--- 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 => _"},