Mercurial Mercurial > repos > isabelle / comparison
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/HOLCF/Universal.thy
changeset 36452 d37c6eed8117
parent 36176 3fe7e97ccca8
child 39974 b525988432e9
equal deleted inserted replaced
36451:ddc965e172c4 36452:d37c6eed8117 
   338 by (rule udom.completion_approx_eq_principal)
 
   338 by (rule udom.completion_approx_eq_principal)
 
   339 
   339 
   340 
   340 
   341 subsection {* Universality of \emph{udom} *}
 
   341 subsection {* Universality of \emph{udom} *}
 
   342 
   342 
   343 defaultsort bifinite
 
   343 default_sort bifinite
 
   344 
   344 
   345 subsubsection {* Choosing a maximal element from a finite set *}
 
   345 subsubsection {* Choosing a maximal element from a finite set *}
 
   346 
   346 
   347 lemma finite_has_maximal:
 
   347 lemma finite_has_maximal:
 
   348   fixes A :: "'a::po set"
 
   348   fixes A :: "'a::po set"
isabelle