X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.lang;h=399d5631b60b7250c337c0665fc7d22905054c87;hb=b0eb62e60a2fd73ba39c7a0df112f04131528602;hp=ea9d318283a14d42ab5ff3283a1eb899815ef7db;hpb=7ed62d94780c881c3ee056418b00ad5e9f739f15;p=helm.git diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index ea9d31828..399d5631b 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -75,13 +75,15 @@ + + implied + theorem record definition inductive coinductive - let fact lemma remark @@ -116,6 +118,7 @@ coinductive constraint corec + cyclic default discriminator for @@ -134,6 +137,7 @@ on precedence qed + defined rec record return