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/Lexord.thy
changeset 77955 c4677a6aae2c
parent 75244 f70b1a2c2783 
--- a/src/HOL/Library/Lexord.thy	Tue May 02 14:19:34 2023 +0200
+++ b/src/HOL/Library/Lexord.thy	Tue May 02 19:49:17 2023 +0200
@@ -153,7 +153,7 @@
     and less_list = lex.lex_less ..
 
 instance
-  by (rule class.preorder.of_class.intro, rule preordering_preorderI, fact lex.preordering)
+  by (rule preorder.intro_of_class, rule preordering_preorderI, fact lex.preordering)
 
 end
 
@@ -171,7 +171,7 @@
 qed
 
 instance list :: (order) order
-  by (rule class.order.of_class.intro, rule ordering_orderI, fact lex.ordering)
+  by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering)
 
 export_code \<open>(\<le>) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> \<open>(<) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> in Haskell
isabelle