# HG changeset patch
# User wenzelm
# Date 1484665907 -3600
# Node ID 5db5b8cf6dc6a1856025a90b40e9caa9a682458b
# Parent  eb6ad9301841517a7af897ee6944d9bbf61c7f77
removed some old ASCII syntax;

diff -r eb6ad9301841 -r 5db5b8cf6dc6 NEWS
--- a/NEWS	Tue Jan 17 16:11:24 2017 +0100
+++ b/NEWS	Tue Jan 17 16:11:47 2017 +0100
@@ -27,6 +27,16 @@
 
 *** HOL ***
 
+* Some old and rarely used ASCII replacement syntax has been removed.
+INCOMPATIBILITY, standard syntax with symbols should be used instead.
+The subsequent commands help to reproduce the old forms, e.g. to
+simplify porting old theories:
+
+syntax (ASCII)
+  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
+  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
+  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
+
 * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
 INCOMPATIBILITY.
 
diff -r eb6ad9301841 -r 5db5b8cf6dc6 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:24 2017 +0100
+++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:47 2017 +0100
@@ -22,9 +22,6 @@
 abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
   where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
 
-syntax (ASCII)
-  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
-  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
 syntax
   "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
   "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
@@ -349,8 +346,6 @@
 
 abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
 
-syntax (ASCII)
-  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
 syntax
   "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
 translations