# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1574956314 0
# Node ID 11e1e273eaad5cee1c8451b5554756a0bd4d9ec3
# Parent  b4d409c65a769c6210dba0e057edad108ed22883
A more informative comment

diff -r b4d409c65a76 -r 11e1e273eaad src/HOL/ex/SOS.thy
--- a/src/HOL/ex/SOS.thy	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/HOL/ex/SOS.thy	Thu Nov 28 15:51:54 2019 +0000
@@ -124,7 +124,7 @@
   by sos
 
 lemma "(x::real) - y - 2 * x^4 = 0 \<and> 0 \<le> x \<and> x \<le> 2 \<and> 0 \<le> y \<and> y \<le> 3 \<longrightarrow> y\<^sup>2 - 7 * y - 12 * x + 17 \<ge> 0"
-  oops (*Too hard?*)
+  oops (*Too hard; left it running for 80 minutes -- LCP*)
 
 lemma "(0::real) \<le> x \<longrightarrow> (1 + x + x\<^sup>2) / (1 + x\<^sup>2) \<le> 1 + x"
   by sos