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)"