X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.lang;h=caffee3f175f29afcc00f7db655873a9426d88f6;hb=b284579a0c4d45bc8483f295434a465ca685f444;hp=fbb21d6d19ba3d4232a91b3dd8554888188eb15f;hpb=e4ce76f25622fade1f74432537acff9daef251d8;p=helm.git diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index fbb21d6d1..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 @@ -169,6 +169,7 @@ focus unfocus progress + skip @@ -178,6 +179,7 @@ check hint set + auto