author wenzelm Wed, 31 Jan 2018 21:05:47 +0100 changeset 67558 c46910a6bfce parent 67557 a965ccf7414e child 67559 833d154ab189
proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";
```--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jan 31 14:20:39 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jan 31 21:05:47 2018 +0100
@@ -750,7 +750,7 @@
local
open Conv
val concl = Thm.dest_arg o Thm.cprop_of
-  fun simple_cterm_ord t u = Term_Ord.fast_term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
in
(* FIXME: Replace tryfind by get_first !! *)
fun real_nonlinear_prover proof_method ctxt =
@@ -851,7 +851,7 @@

local
open Conv
-  fun simple_cterm_ord t u = Term_Ord.fast_term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
val concl = Thm.dest_arg o Thm.cprop_of
val shuffle1 =
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"```