@@ -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.