X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.tex;h=09b1f0b79a80a379f473ac2a8153e28e518f135e;hb=22360727aa1b513bd1529ef63aadb59b92095922;hp=8ed71abe69bee79f4b2a8763c43d8fa67fbc8abd;hpb=2a81818cb4b942c35a1cfa88121e561309e59172;p=helm.git diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index 8ed71abe6..09b1f0b79 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -283,8 +283,8 @@ depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a pipline of three levels: the concrete syntax level (level 0) is the one the user has to deal with when inserting CIC terms; the abstract syntax level (level 2) is an internal representation which intuitively encodes mathematical formulae at -the content level \NOTE{rif. per\\ content}; the formal mathematics level (level -3) is the CIC encoding of terms. +the content level~\cite{adams}~\cite{mkm-structure}; the formal mathematics +level (level 3) is the CIC encoding of terms. Requirement (1) is addressed by a built-in concrete syntax for terms, described in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a