X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fletrec.ma;h=55933cd31bf8aeb42aa0834e890fedf877cf958d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=24b63593cc92e9595c257d59df2758ee94c631e6;hpb=d8cf90b2aa66f0170db0c35b8b5d53a1eb74008e;p=helm.git diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma index 24b63593c..55933cd31 100644 --- a/helm/matita/tests/letrec.ma +++ b/helm/matita/tests/letrec.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/letrec/". + alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".