src/ZF/Finite.thy
changeset 80917 2a77bc3b4eac
parent 76217 8655344f1cf6
--- a/src/ZF/Finite.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Finite.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -19,7 +19,7 @@
 
 consts
   Fin       :: "i\<Rightarrow>i"
-  FiniteFun :: "[i,i]\<Rightarrow>i"         (\<open>(_ -||>/ _)\<close> [61, 60] 60)
+  FiniteFun :: "[i,i]\<Rightarrow>i"  (\<open>(\<open>notation=\<open>infix -||>\<close>\<close>_ -||>/ _)\<close> [61, 60] 60)
 
 inductive
   domains   "Fin(A)" \<subseteq> "Pow(A)"