-the usual mathematical notation, peeking constants and symbols from the
-whole library; direct manipulation of terms, with a corresponding elaborated
-textual syntax to record the user actions; a fine-grained execution of
-tacticals to simplify script structuring and replaying; an integrated
-browser to navigate the hypertext formed by the concepts in the library,
-integrated with natural language rendering of proof; compatibility with
-the library of the Coq proof assistant.
-
-In the near future we plan to continue development focusing on and enhanching
-the peculiarities of \MATITA, starting from its document centric phylosophy.
+the usual mathematical notation, using constants and symbols from the
+whole library; direct manipulation of terms in the GUI,
+with a corresponding elaborated
+textual syntax to record user actions; fine-grained execution of
+tacticals to simplify script structuring and replaying; a browsing
+tool to navigate the hypertext formed by the concepts in the library,
+integrated with natural language rendering of proofs; compatibility with
+the library of the \COQ{} proof assistant.
+
+In the near future we plan to continue the development focusing on and enhancing
+the peculiarities of \MATITA, starting from its document-centric philosophy.