last commit for helena 0.8.2

[helm.git] / helm / software / helena / examples / automath / omega.aut

diff --git a/helm/software/helena/examples/automath/omega.aut b/helm/software/helena/examples/automath/omega.aut
deleted file mode 100644 (file)
index 9e6c30e..0000000
--- a/helm/software/helena/examples/automath/omega.aut
+++ /dev/null
@@ -1,8 +0,0 @@
-# This book is not valid in AUT-QE because [y:'type'] is not allowed
-# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
-# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
-
-+l
-@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
-@ Omega := <Delta>Delta : 'type'
--l