X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=ce58853f7749f710461247d64dcbaacf375a1c53;hb=44f4e888646ac95752bbd8c3e7b9b4b48209b1a6;hp=57298c377974123e06b9e4ba7e40e57310a992ab;hpb=d0b2bceffedce633f496b4e4fcc557be73fbfe1d;p=helm.git
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 57298c377..ce58853f7 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -26,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.