X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.lang;h=0c181ee4480269bf55ec473df745108fc03e825e;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=a20193f1feb76ae32a6a1307ffa9197e5c4f9f69;hpb=f1a2aec37db8f0a4da540a027cf91554e27ba88c;p=helm.git diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index a20193f1f..0c181ee44 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -1,13 +1,9 @@ - + \ - - %% - - \(\* \*\) @@ -24,23 +20,34 @@ lemma fact remark + variant alias + and + as coercion coinductive corec - in + default + for + include inductive + in + interpretation let match + names + notation + on qed rec record + return + to + using with - - @@ -58,6 +65,12 @@ \} + + @ + + + \$ + Set @@ -70,21 +83,32 @@ apply assumption auto + paramodulation + clear + clearbody change + compare + constructor contradiction cut + decide equality decompose discriminate elim elimType exact exists + fail fold fourier + fwd + generalize goal + id injection intro intros + lapply left letin normalize @@ -92,15 +116,25 @@ reflexivity replace rewrite - right ring - simmetry + right + symmetry simplify split + to transitivity + unfold whd + + try + solve + do + repeat + first + + print @@ -136,7 +170,12 @@ Assign land lor + lnot + liff subst + vdash + iforall + iexists @@ -145,4 +184,3 @@ -