]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/automath/Omega.aut
- dehypenation involves helena as well
[helm.git] / helm / software / helena / src / automath / Omega.aut
index 2466a606e0bde14fb594e8f2d1130c646e04ac89..727f9fe6a2079fc29008ada51614d434c55bedfc 100644 (file)
@@ -1,8 +1,8 @@
-# The lambda-term \Omega
+# The term \Omega
 # 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
+# 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 unrestricted sort inclusion 
+# This book is valid in \lambda\delta with unrestricted sort inclusion 
 
 +l 
 @ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'