--- a/src/ZF/QUniv.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/ZF/QUniv.thy Mon Apr 25 16:09:26 2016 +0200
@@ -58,7 +58,7 @@
apply (rule Transset_eclose [THEN Transset_univ])
done
-(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
+(*Key property for proving A_subset_quniv; requires eclose in definition of quniv*)
lemma univ_subset_quniv: "univ(A) \<subseteq> quniv(A)"
apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
apply (rule univ_eclose_subset_quniv)