X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fnotation.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fnotation.ma;h=d4302a32a8b6d350aff395297974666ec774a62c;hb=fd991956035d0f1b663aab48325097e53ed9e00e;hp=375d06abc776e6af2eb9c444c7619bbd50053caf;hpb=4a0e7bf321b9a1601b82237b086aa2ab641ac880;p=helm.git diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index 375d06abc..d4302a32a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -1,17 +1,20 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* Syntax *******************************************************************) +(* Grammar ******************************************************************) notation "hvbox( ⋆ )" non associative with precedence 90