src/ZF/Constructible/Normal.thy

--- a/src/ZF/Constructible/Normal.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Constructible/Normal.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -463,7 +463,7 @@
 numbers.\<close>
 
 definition
-  Aleph :: "i \<Rightarrow> i"  (\<open>\<aleph>_\<close> [90] 90) where
+  Aleph :: "i \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>prefix \<aleph>\<close>\<close>\<aleph>_)\<close> [90] 90) where
     "Aleph(a) \<equiv> transrec2(a, nat, \<lambda>x r. csucc(r))"
 
 lemma Card_Aleph [simp, intro]: