]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/examples/automath/README.txt
level disambiguation cmpleted! the Grafite file is succesfully generated.
[helm.git] / helm / software / helena / examples / automath / README.txt
diff --git a/helm/software/helena/examples/automath/README.txt b/helm/software/helena/examples/automath/README.txt
new file mode 100644 (file)
index 0000000..5d12c46
--- /dev/null
@@ -0,0 +1,5 @@
+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