Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)";
authorwenzelm
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)";
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML file | annotate | diff | comparison | revisions 
--- 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))"
isabelle