--- a/src/HOL/Library/FuncSet.thy Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy Mon Dec 28 21:47:32 2015 +0100
@@ -20,10 +20,10 @@
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
+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 (xsymbols)
+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)
translations
@@ -347,11 +347,12 @@
abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
-syntax
+syntax (ASCII)
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10)
-syntax (xsymbols)
+syntax
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
-translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
+translations
+ "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"