Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped redundant syntax translation rules for big operators
authorhaftmann
Thu, 23 Aug 2018 17:09:37 +0000
changeset 68795 210b687cdbbe
parent 68794 63e84bd8e1f6
child 68796 9ca183045102
dropped redundant syntax translation rules for big operators
src/HOL/Complete_Lattices.thy file | annotate | diff | comparison | revisions
src/HOL/GCD.thy file | annotate | diff | comparison | revisions
src/HOL/Lattices_Big.thy file | annotate | diff | comparison | revisions 
--- 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)"
 
--- 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)"
 
--- 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