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/Lattices_Big.thy
changeset 68795 210b687cdbbe
parent 68793 462226db648a
child 68796 9ca183045102 
--- a/src/HOL/Lattices_Big.thy	Thu Aug 23 16:45:19 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Thu Aug 23 17:09:37 2018 +0000
@@ -490,11 +490,9 @@
 
 translations
   "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
-  "MIN x. B"     \<rightleftharpoons> "CONST MINIMUM CONST UNIV (\<lambda>x. B)"
   "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
   "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
   "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
-  "MAX x. B"     \<rightleftharpoons> "CONST MAXIMUM CONST UNIV (\<lambda>x. B)"
   "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
   "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
isabelle