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.
tuned;
authorwenzelm
Thu, 01 Feb 2018 17:21:58 +0100
changeset 67563 6e5316a43079
parent 67562 2427d3e72b6e
child 67564 d615e9ca77dc
tuned;
src/HOL/Decision_Procs/Dense_Linear_Order.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:15:07 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:21:58 2018 +0100
@@ -894,7 +894,8 @@
     | earlier (h::t) (x, y) =
         if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
 
-  val earlier_ord = make_ord o earlier;
+  fun earlier_ord vs (x, y) =
+    if x aconvc y then EQUAL else make_ord (earlier vs) (x, y);
 
 fun dest_frac ct =
   case Thm.term_of ct of
isabelle