examples/automath/README.txt

   1 This directory contains:
   2
   3 grundlagen_0.aut: original specification valid in AutQE with η-reduction enabled
   4 grundlagen_1.aut: "η-equivalent" specification valid also in λδ version 3
   5 grundlagen_2.aut: "η-equivalent" specification valid also in a Pure Type System
   6
   7 Omega.aut       : the invalid term \Omega