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/Library/List_lexord.thy
changeset 22316 f662831459de
parent 22177 515021e98684
child 22483 86064f2f2188 
--- a/src/HOL/Library/List_lexord.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -17,14 +17,14 @@
 
 instance list :: (order) order
   apply (intro_classes, unfold list_ord_defs)
-     apply (rule disjI2, safe)
-    apply (blast intro: lexord_trans transI order_less_trans)
-   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
-    apply simp
-   apply (blast intro: lexord_trans transI order_less_trans)
+  apply safe
   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
   apply simp
   apply assumption
+  apply (blast intro: lexord_trans transI order_less_trans)
+  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
+  apply simp
+  apply (blast intro: lexord_trans transI order_less_trans)
   done
 
 instance list :: (linorder) linorder
isabelle