]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/automath/Omega.aut
some renaming. final commit for version 0.8.0
[helm.git] / helm / software / lambda-delta / automath / Omega.aut
index 661154db9db58b2cce3d5c031988474c18d73554..2466a606e0bde14fb594e8f2d1130c646e04ac89 100644 (file)
@@ -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'