refactoring: helena sources are now in a dedicated directory

[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
deleted file mode 100644 (file)
index 2466a60..0000000
--- a/helm/software/lambda-delta/automath/Omega.aut
+++ /dev/null
@@ -1,10 +0,0 @@
-# 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
-#    valid if sort inclusion is allowed on the term backbone only
-# This book is valid in lambda-delta with unrestricted sort inclusion 
-
-+l 
-@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
-  Omega := <Delta>Delta             : 'type'
--l