X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Frecord.ma;h=ed9ecfed89044bb99ba17cf90fcb14f411dab30e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=61dec1d7e34671c1ca7a1d890b10f789ab43bec0;hpb=522bfe4fd22804ff7fb0013697721504003a6606;p=helm.git diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma index 61dec1d7e..ed9ecfed8 100644 --- a/helm/matita/tests/record.ma +++ b/helm/matita/tests/record.ma @@ -1,3 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/record/". + record empty : Type \def {}. inductive True : Prop \def I: True. @@ -20,4 +36,4 @@ record paperino: Prop \def { paolo : Type; pippo : paolo \to paolo; piero : True -}. \ No newline at end of file +}.