src/ZF/QUniv.thy
changeset 76215 a642599ffdea
parent 76214 0c18df79b1c8
child 76216 9fc34f76b4e8
--- a/src/ZF/QUniv.thy	Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/QUniv.thy	Tue Sep 27 17:46:52 2022 +0100
@@ -20,7 +20,7 @@
   case_eqns     qcase_QInl qcase_QInr
 
 definition
-  quniv :: "i => i"  where
+  quniv :: "i \<Rightarrow> i"  where
    "quniv(A) \<equiv> Pow(univ(eclose(A)))"