X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.lang;h=ea9a08e1337cfffc3df116bc0ca487bab177abec;hb=f16a572ff09aa3a0f9c8103914616ed49e7b4c29;hp=964ddeb1d5c5c04134294ad4ab1997804bf24aca;hpb=9cce83f0364d04a98cc5e9dfc80ce47ce3c68686;p=helm.git diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 964ddeb1d..ea9a08e13 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -75,6 +75,9 @@ + + implied + theorem record @@ -109,6 +112,7 @@ alias and as + associative coercion prefer nocomposites @@ -124,15 +128,20 @@ inverter in interpretation + left let match names - notation + non + notation on + precedence qed + defined rec record return + right source to universe