X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.lang;h=6a24b9aed1089ab85ef68df919e1635d54850676;hb=bac3136bf99a18374b91e1ec900e455567e8f741;hp=d59ab06a95ad3fd04363b82efebcf654e3bf6bee;hpb=8657e4db50a00431c1ae3d2fd5c7d4d55ea488b5;p=helm.git diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index d59ab06a9..6a24b9aed 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -5,7 +5,7 @@ \(\*\*[^\)] - [^\(]\*\*\) + [^\(]\*\) @@ -22,12 +22,25 @@ variant axiom + + + ntheorem + nrecord + ndefinition + ninductive + ncoinductive + nlet + nlemma + naxiom + alias and as coercion + prefer + nocomposites coinductive corec default @@ -35,6 +48,7 @@ include include' inductive + inverter in interpretation let @@ -46,11 +60,20 @@ rec record return + source to using with + + unification + hint + ncoercion + ninverter + nqed + + \[ @@ -77,11 +100,23 @@ Set Prop Type + CProp + + + + Prop + Type[0] + CProp[0] + Type[1] + CProp[1] + Type[2] + CProp[2] absurd apply + applyP assumption autobatch cases @@ -112,7 +147,6 @@ left letin normalize - reduce reflexivity replace rewrite @@ -156,6 +190,23 @@ obtain conclude done + rule + + + + napply + ncases + nletin + nauto + nelim + nwhd + nnormalize + nassumption + ngeneralize + nchange + nrewrite + ncut + nlapply @@ -175,9 +226,19 @@ inline procedural check + eval hint set auto + nodefaults + coercions + comments + debug + cr + + + + ncheck