# HG changeset patch
# User wenzelm
# Date 1728423066 -7200
# Node ID d90869a85f60baa46dc935926a844fd89097ae04
# Parent  d23f5a898084a86f53b5686095ef97fa88271f89
more syntax bundles;

diff -r d23f5a898084 -r d90869a85f60 NEWS
--- a/NEWS	Tue Oct 08 22:56:27 2024 +0200
+++ b/NEWS	Tue Oct 08 23:31:06 2024 +0200
@@ -75,6 +75,7 @@
   unbundle no abs_syntax
   unbundle no floor_ceiling_syntax
   unbundle no uminus_syntax
+  unbundle no funcset_syntax
 
 This is more robust than individual 'no_syntax' / 'no_notation'
 commands, which need to copy mixfix declarations from elsewhere and thus
diff -r d23f5a898084 -r d90869a85f60 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Oct 08 22:56:27 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Oct 08 23:31:06 2024 +0200
@@ -19,8 +19,13 @@
 definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
   where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
 
-abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr \<open>\<rightarrow>\<close> 60)
-  where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
+abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"
+  where "funcset A B \<equiv> Pi A (\<lambda>_. B)"
+
+open_bundle funcset_syntax
+begin
+notation funcset  (infixr \<open>\<rightarrow>\<close> 60)
+end
 
 syntax
   "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (\<open>(3\<Pi> _\<in>_./ _)\<close>   10)