From 22360727aa1b513bd1529ef63aadb59b92095922 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 15 Nov 2005 18:17:19 +0000 Subject: [PATCH 1/1] added content level ref --- helm/papers/matita/Makefile | 2 +- helm/papers/matita/matita.tex | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile index 07747771a..bfae83c3a 100644 --- a/helm/papers/matita/Makefile +++ b/helm/papers/matita/Makefile @@ -17,7 +17,7 @@ TEXS = matita.tex RUNS = 1 # do you need bibtex? -BIBTEX = no +BIBTEX = yes # would you like to use pdflatex? PDF_VIA_PDFLATEX = yes 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 -- 2.39.2