X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.lang;h=f74da76e74f3cab07d94f93a6f3df70336eb1cfe;hb=d1c92207efd70bed92a69014c0264bee717992ba;hp=d2015ee3e4320df4c64b89274acfe09297947776;hpb=e32693f30563379989b75b53c3be088396b732da;p=helm.git diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index d2015ee3e..f74da76e7 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -28,6 +28,7 @@ coinductive corec in + on inductive let match @@ -35,8 +36,10 @@ rec record with - - + and + to + as + using @@ -66,22 +69,31 @@ apply assumption auto + 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 @@ -94,6 +106,7 @@ symmetry simplify split + to transitivity whd @@ -134,6 +147,7 @@ land lor subst + vdash