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/Poly_Mapping.thy
changeset 77955 c4677a6aae2c
parent 76987 4c275405faae
child 80095 0f9cd1a5edbe 
--- a/src/HOL/Library/Poly_Mapping.thy	Tue May 02 14:19:34 2023 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy	Tue May 02 19:49:17 2023 +0200
@@ -910,7 +910,7 @@
   is "\<lambda>f g. less_fun f g \<or> f = g"
   .
 
-instance proof (rule class.Orderings.linorder.of_class.intro)
+instance proof (rule linorder.intro_of_class)
   show "class.linorder (less_eq :: (_ \<Rightarrow>\<^sub>0 _) \<Rightarrow> _) less"
   proof (rule linorder_strictI, rule order_strictI)
     fix f g h :: "'a \<Rightarrow>\<^sub>0 'b"
isabelle