X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.lang;h=caffee3f175f29afcc00f7db655873a9426d88f6;hb=b284579a0c4d45bc8483f295434a465ca685f444;hp=72055f386a680e2bca3fad9690fb813693bdf5c8;hpb=9d2d712272880222b3efa3b9d97132f6eeff0c8a;p=helm.git diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 72055f386..caffee3f1 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -28,6 +28,7 @@ and as coercion + nocomposites coinductive corec default @@ -77,18 +78,19 @@ Set Prop Type + CProp absurd apply assumption - auto - paramodulation + autobatch cases clear clearbody change + compose constructor contradiction cut @@ -103,7 +105,6 @@ fourier fwd generalize - goal id intro intros @@ -122,7 +123,6 @@ symmetry simplify split - subst to transitivity unfold @@ -165,11 +165,11 @@ solve do repeat - end first focus unfocus progress + skip @@ -179,6 +179,7 @@ check hint set + auto