X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=ce58853f7749f710461247d64dcbaacf375a1c53;hb=44f4e888646ac95752bbd8c3e7b9b4b48209b1a6;hp=30830764c887d54ad30445ca868b9770ce19ab05;hpb=3f55b3f76a5228ec5b97664469941736b9fb0202;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 30830764c..ce58853f7 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -7,6 +7,7 @@ +
@@ -25,10 +26,10 @@ Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive Constructions (CIC). It can re-use - mathematical concepts produced by other proof assistants like - Coq and encoded in an - XML encoding of CIC. The interaction - paradigm of Matita is familiar, being inspired by CtCoq and + mathematical concepts produced by other proof assistants (e.g. + Coq) when encoded in an + XML representation of CIC. The + interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof General. Its proof language is procedural in the same spirit of LCF.