X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fautomath%2FREADME;fp=helm%2Fsoftware%2Fhelena%2Fexamples%2Fautomath%2FREADME;h=8b6c026eada17b9ba4dea5802b2dd5d8cfee4c8f;hb=c6aece41fb3865f411bfe2a886b3b3cfb519031f;hp=0000000000000000000000000000000000000000;hpb=6abec8ca6434937e46e098ed946bc6ed307f022b;p=helm.git

diff --git a/helm/software/helena/examples/automath/README b/helm/software/helena/examples/automath/README
new file mode 100644
index 000000000..8b6c026ea
--- /dev/null
+++ b/helm/software/helena/examples/automath/README
@@ -0,0 +1,7 @@
+This directory contains:
+
+grundlagen_0.aut: original specification valid in AutQE with η-reduction enabled
+grundlagen_1.aut: "η-equivalent" specification valid also in λδ version 3
+grundlagen_2.aut: "η-equivalent" specification valid also in a Pure Type System
+
+Omega.aut       : the invalid term \Omega