Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Dense_Linear_Order.thy
changeset 67565 e13378b304dd
parent 67563 6e5316a43079
child 69597 ff784d5a5bfb 
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:27:13 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 20:29:53 2018 +0100
@@ -895,7 +895,9 @@
         if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
 
   fun earlier_ord vs (x, y) =
-    if x aconvc y then EQUAL else make_ord (earlier vs) (x, y);
+    if x aconvc y then EQUAL
+    else if earlier vs (x, y) then LESS
+    else GREATER;
 
 fun dest_frac ct =
   case Thm.term_of ct of
isabelle