X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FOmega.aut;h=2466a606e0bde14fb594e8f2d1130c646e04ac89;hb=ab739c4972971725f59c52275a3257ebf524143f;hp=661154db9db58b2cce3d5c031988474c18d73554;hpb=c52a5748465e24374aec569bf74fc85e5bbb075a;p=helm.git

diff --git a/helm/software/lambda-delta/automath/Omega.aut b/helm/software/lambda-delta/automath/Omega.aut
index 661154db9..2466a606e 100644
--- a/helm/software/lambda-delta/automath/Omega.aut
+++ b/helm/software/lambda-delta/automath/Omega.aut
@@ -2,7 +2,7 @@
 # This book is not accepted in AUT-QE because [y:'type'] is not allowed
 # This book is accepted in lambda-delta with sort inclusion but Omega is not
 #    valid if sort inclusion is allowed on the term backbone only
-# This book is valid in lambda-delta with sort inclusion allowed everywhere 
+# This book is valid in lambda-delta with unrestricted sort inclusion 
 
 +l 
 @ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'