X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FBase-2%2Ftypes%2Fdefs2.mma;fp=matita%2Fcontribs%2FLAMBDA-TYPES%2FBase-2%2Ftypes%2Fdefs2.mma;h=594edd269d6934a5992b5eeca4629904ece283cb;hb=711e170c2deaa92289d9d4eb7c0e8aedbe62b5cb;hp=0000000000000000000000000000000000000000;hpb=fe0aaba722c4a752585bc1046e219b452a2d452b;p=helm.git diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma new file mode 100644 index 000000000..594edd269 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "preamble.ma". + + +(* object and3 not inlined *) + + +(* object and4 not inlined *) + + +(* object or3 not inlined *) + + +(* object or4 not inlined *) + + +(* object ex3 not inlined *) + + +(* object ex4 not inlined *) + + +(* object ex_2 not inlined *) + + +(* object ex2_2 not inlined *) + + +(* object ex3_2 not inlined *) + + +(* object ex4_2 not inlined *) + + +(* object ex_3 not inlined *) + + +(* object ex2_3 not inlined *) + + +(* object ex3_3 not inlined *) + + +(* object ex4_3 not inlined *) + + +(* object ex3_4 not inlined *) + + +(* object ex4_4 not inlined *) + + +(* object ex4_5 not inlined *) + + +(* object ex5_5 not inlined *) + + +(* object ex6_6 not inlined *) + + +(* object ex6_7 not inlined *) +