# HG changeset patch
# User haftmann
# Date 1535044177 0
# Node ID 210b687cdbbe2e6248aea542dad1ddf9a5c9bb25
# Parent  63e84bd8e1f68f1ef32b15ca3cc61f76db6a183e
dropped redundant syntax translation rules for big operators

diff -r 63e84bd8e1f6 -r 210b687cdbbe src/HOL/Complete_Lattices.thy
--- 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)"
 
diff -r 63e84bd8e1f6 -r 210b687cdbbe src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Aug 23 16:45:19 2018 +0200
+++ b/src/HOL/GCD.thy	Thu Aug 23 17:09:37 2018 +0000
@@ -161,13 +161,12 @@
   "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
+
 translations
   "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
-  "GCD x. B"     \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)"
   "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
   "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
   "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
-  "LCM x. B"     \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. B)"
   "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
   "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
 
diff -r 63e84bd8e1f6 -r 210b687cdbbe src/HOL/Lattices_Big.thy
--- 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)"