src/ZF/Constructible/Normal.thy

--- a/src/ZF/Constructible/Normal.thy	Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Constructible/Normal.thy	Sat Oct 10 22:08:43 2015 +0200
@@ -456,12 +456,9 @@
 numbers.\<close>
 
 definition
-  Aleph :: "i => i" where
+  Aleph :: "i => i"  ("\<aleph>_" [90] 90) where
     "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
 
-notation (xsymbols)
-  Aleph  ("\<aleph>_" [90] 90)
-
 lemma Card_Aleph [simp, intro]:
      "Ord(a) ==> Card(Aleph(a))"
 apply (erule trans_induct3)