NEWS
changeset 64917 5db5b8cf6dc6
parent 64900 3687036107cd
child 64986 b81a048960a3
     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