# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID 48609a6af1a0282bda914123a21a6abeaccadbcc
# Parent  559f4552880484877b7163d8cf62abf302db38db
removed relics of ASCII syntax for indexed big operators

diff -r 559f45528804 -r 48609a6af1a0 NEWS
--- a/NEWS	Fri Jun 14 08:34:27 2019 +0000
+++ b/NEWS	Fri Jun 14 08:34:27 2019 +0000
@@ -1,3 +1,5 @@
+
+
 Isabelle NEWS -- history of user-relevant changes
 =================================================
 
@@ -7,6 +9,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* ASCII membership syntax concerning big operators for infimum
+and supremum is gone.  INCOMPATIBILITY.
+
+
 
 New in Isabelle2019 (June 2019)
 -------------------------------
diff -r 559f45528804 -r 48609a6af1a0 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -7,7 +7,7 @@
 
 definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
   where "nhdsin X a =
-           (if a \<in> topspace X then (INF S:{S. openin X S \<and> a \<in> S}. principal S) else bot)"
+           (if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"
 
 definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
   where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
@@ -21,7 +21,7 @@
   "eventually P (nhdsin X a) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
 proof (cases "a \<in> topspace X")
   case True
-  hence "nhdsin X a = (INF S:{S. openin X S \<and> a \<in> S}. principal S)"
+  hence "nhdsin X a = (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S)"
     by (simp add: nhdsin_def)
   also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
     using True by (subst eventually_INF_base) (auto simp: eventually_principal)
diff -r 559f45528804 -r 48609a6af1a0 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Complete_Lattices.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -20,12 +20,6 @@
 class Sup =
   fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>")
 
-syntax (ASCII)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
-
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _\<in>_./ _)" [0, 0, 10] 10)
diff -r 559f45528804 -r 48609a6af1a0 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -4081,7 +4081,7 @@
   by (simp add: dist_fls_def)
 
 definition uniformity_fls_def [code del]:
-  "(uniformity :: ('a fls \<times> 'a fls) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity :: ('a fls \<times> 'a fls) filter) = (INF e \<in> {0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_fls_def' [code del]:
   "open (U :: 'a fls set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"