--- 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)
-------------------------------
--- 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)
--- 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)
--- 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)"