diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -25,6 +25,9 @@
 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)
+syntax_consts
+  "_Pi" \<rightleftharpoons> Pi and
+  "_lam" \<rightleftharpoons> restrict
 translations
   "\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
   "\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
@@ -350,6 +353,8 @@
 
 syntax
   "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
+syntax_consts
+  "_PiE" \<rightleftharpoons> Pi\<^sub>E
 translations
   "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"