X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.lang;h=399d5631b60b7250c337c0665fc7d22905054c87;hb=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=29831639baec568fe21c050bc9bb5e2ee1041b0c;hpb=514f515ecb8765c68720e880460c2457898d74dc;p=helm.git diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 29831639b..399d5631b 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -75,13 +75,15 @@ + + implied + theorem record definition inductive coinductive - let fact lemma remark @@ -109,11 +111,14 @@ alias and as + associative coercion prefer nocomposites coinductive + constraint corec + cyclic default discriminator for @@ -123,18 +128,24 @@ inverter in interpretation + left let match names - notation + non + notation on + precedence qed + defined rec record return + right source to - using + universe + using with