Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/FuncSet.thy
changeset 81135 d90869a85f60
parent 80914 d97fdabd9e2b
child 81142 6ad2c917dd2e 
--- 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)
isabelle