X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.lang;h=136efe5736aa0bc99fccaac2e18ec54f081a34c8;hb=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;hp=29831639baec568fe21c050bc9bb5e2ee1041b0c;hpb=514f515ecb8765c68720e880460c2457898d74dc;p=helm.git diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 29831639b..136efe573 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,10 +111,12 @@ alias and as + associative coercion prefer nocomposites coinductive + constraint corec default discriminator @@ -123,18 +127,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