removed relics of ASCII syntax for indexed big operators
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (4 weeks ago)
changeset 7033748609a6af1a0
parent 70336 559f45528804
child 70338 c832d431636b
removed relics of ASCII syntax for indexed big operators
NEWS
src/HOL/Analysis/Abstract_Limits.thy
src/HOL/Complete_Lattices.thy
src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
     1.1 --- a/NEWS	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/NEWS	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -1,3 +1,5 @@
     1.4 +
     1.5 +
     1.6  Isabelle NEWS -- history of user-relevant changes
     1.7  =================================================
     1.8  
     1.9 @@ -7,6 +9,12 @@
    1.10  New in this Isabelle version
    1.11  ----------------------------
    1.12  
    1.13 +*** HOL ***
    1.14 +
    1.15 +* ASCII membership syntax concerning big operators for infimum
    1.16 +and supremum is gone.  INCOMPATIBILITY.
    1.17 +
    1.18 +
    1.19  
    1.20  New in Isabelle2019 (June 2019)
    1.21  -------------------------------
     2.1 --- a/src/HOL/Analysis/Abstract_Limits.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/Analysis/Abstract_Limits.thy	Fri Jun 14 08:34:27 2019 +0000
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
     2.6    where "nhdsin X a =
     2.7 -           (if a \<in> topspace X then (INF S:{S. openin X S \<and> a \<in> S}. principal S) else bot)"
     2.8 +           (if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"
     2.9  
    2.10  definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
    2.11    where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
    2.12 @@ -21,7 +21,7 @@
    2.13    "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))"
    2.14  proof (cases "a \<in> topspace X")
    2.15    case True
    2.16 -  hence "nhdsin X a = (INF S:{S. openin X S \<and> a \<in> S}. principal S)"
    2.17 +  hence "nhdsin X a = (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S)"
    2.18      by (simp add: nhdsin_def)
    2.19    also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    2.20      using True by (subst eventually_INF_base) (auto simp: eventually_principal)
     3.1 --- a/src/HOL/Complete_Lattices.thy	Fri Jun 14 08:34:27 2019 +0000
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Fri Jun 14 08:34:27 2019 +0000
     3.3 @@ -20,12 +20,6 @@
     3.4  class Sup =
     3.5    fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>")
     3.6  
     3.7 -syntax (ASCII)
     3.8 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
     3.9 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    3.10 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    3.11 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    3.12 -
    3.13  syntax
    3.14    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    3.15    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _\<in>_./ _)" [0, 0, 10] 10)
     4.1 --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Jun 14 08:34:27 2019 +0000
     4.2 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Jun 14 08:34:27 2019 +0000
     4.3 @@ -4081,7 +4081,7 @@
     4.4    by (simp add: dist_fls_def)
     4.5  
     4.6  definition uniformity_fls_def [code del]:
     4.7 -  "(uniformity :: ('a fls \<times> 'a fls) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
     4.8 +  "(uniformity :: ('a fls \<times> 'a fls) filter) = (INF e \<in> {0 <..}. principal {(x, y). dist x y < e})"
     4.9  
    4.10  definition open_fls_def' [code del]:
    4.11    "open (U :: 'a fls set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"