]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/examples/automath/README
additional commit for version 0.8.2
[helm.git] / helm / software / helena / examples / automath / README
diff --git a/helm/software/helena/examples/automath/README b/helm/software/helena/examples/automath/README
new file mode 100644 (file)
index 0000000..8b6c026
--- /dev/null
@@ -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