more syntax bundles;
authorwenzelm
Tue, 08 Oct 2024 23:31:06 +0200
changeset 81135 d90869a85f60
parent 81134 d23f5a898084
child 81136 2b949a3bfaac
more syntax bundles;
NEWS
src/HOL/Library/FuncSet.thy
--- 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
--- 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)