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/Complete_Lattices.thy
changeset 68795 210b687cdbbe
parent 67829 2a6ef5ba4822
child 68796 9ca183045102 
--- a/src/HOL/Complete_Lattices.thy	Thu Aug 23 16:45:19 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:37 2018 +0000
@@ -90,11 +90,9 @@
 
 translations
   "\<Sqinter>x y. B"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. B"
-  "\<Sqinter>x. B"     \<rightleftharpoons> "CONST INFIMUM CONST UNIV (\<lambda>x. B)"
   "\<Sqinter>x. B"     \<rightleftharpoons> "\<Sqinter>x \<in> CONST UNIV. B"
   "\<Sqinter>x\<in>A. B"   \<rightleftharpoons> "CONST INFIMUM A (\<lambda>x. B)"
   "\<Squnion>x y. B"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. B"
-  "\<Squnion>x. B"     \<rightleftharpoons> "CONST SUPREMUM CONST UNIV (\<lambda>x. B)"
   "\<Squnion>x. B"     \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
   "\<Squnion>x\<in>A. B"   \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
 
@@ -876,7 +874,6 @@
 
 translations
   "\<Inter>x y. B"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. B"
-  "\<Inter>x. B"    \<rightleftharpoons> "CONST INTER CONST UNIV (\<lambda>x. B)"
   "\<Inter>x. B"    \<rightleftharpoons> "\<Inter>x \<in> CONST UNIV. B"
   "\<Inter>x\<in>A. B"  \<rightleftharpoons> "CONST INTER A (\<lambda>x. B)"
 
@@ -1046,7 +1043,6 @@
 
 translations
   "\<Union>x y. B"   \<rightleftharpoons> "\<Union>x. \<Union>y. B"
-  "\<Union>x. B"     \<rightleftharpoons> "CONST UNION CONST UNIV (\<lambda>x. B)"
   "\<Union>x. B"     \<rightleftharpoons> "\<Union>x \<in> CONST UNIV. B"
   "\<Union>x\<in>A. B"   \<rightleftharpoons> "CONST UNION A (\<lambda>x. B)"
isabelle