basic_rg: bugfix in AST to allow attributes in global entries

[helm.git] / helm / software / lambda-delta / automath / omega.aut

diff --git a/helm/software/lambda-delta/automath/omega.aut b/helm/software/lambda-delta/automath/omega.aut
index 9a41532ce564b28233879b586b3c66c04ec166b2..661154db9db58b2cce3d5c031988474c18d73554 100644 (file)
--- a/helm/software/lambda-delta/automath/omega.aut
+++ b/helm/software/lambda-delta/automath/omega.aut
@@ -1,10 +1,10 @@
-# The lambda-term \omega
+# The lambda-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 sort inclusion allowed everywhere 
 
 +l 
-@ delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
-  omega := <delta>delta             : 'type'
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+  Omega := <Delta>Delta             : 'type'
 -l