removed some old ASCII syntax;
authorwenzelm
Tue Jan 17 16:11:47 2017 +0100 (2017-01-17)
changeset 649175db5b8cf6dc6
parent 64916 eb6ad9301841
child 64918 440f55c3fd55
removed some old ASCII syntax;
NEWS
src/HOL/Library/FuncSet.thy
     1.1 --- a/NEWS	Tue Jan 17 16:11:24 2017 +0100
     1.2 +++ b/NEWS	Tue Jan 17 16:11:47 2017 +0100
     1.3 @@ -27,6 +27,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Some old and rarely used ASCII replacement syntax has been removed.
     1.8 +INCOMPATIBILITY, standard syntax with symbols should be used instead.
     1.9 +The subsequent commands help to reproduce the old forms, e.g. to
    1.10 +simplify porting old theories:
    1.11 +
    1.12 +syntax (ASCII)
    1.13 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
    1.14 +  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
    1.15 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.16 +
    1.17  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
    1.18  INCOMPATIBILITY.
    1.19  
     2.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:24 2017 +0100
     2.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:47 2017 +0100
     2.3 @@ -22,9 +22,6 @@
     2.4  abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
     2.5    where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
     2.6  
     2.7 -syntax (ASCII)
     2.8 -  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
     2.9 -  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    2.10  syntax
    2.11    "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    2.12    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    2.13 @@ -349,8 +346,6 @@
    2.14  
    2.15  abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
    2.16  
    2.17 -syntax (ASCII)
    2.18 -  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
    2.19  syntax
    2.20    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    2.21  translations