From 80eefd160882cc1b968fb41d5f04b278f5dc7f4b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 Jan 2006 12:58:02 +0000 Subject: [PATCH] Typos --- helm/papers/matita/matita2.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 9dca4c677..464e66c0d 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -764,9 +764,9 @@ library. To this aim, Matita uses a sophisticated indexing mechanism for mathemtical items, based on a reach metadata set that has been tuned along the European Project IST-2001-33562 MoWGLI. The metadata set, and the searching facilites built on top of them - collected -in the so called \whelp seach engine - have been +in the so called \WHELP search engine - have been extensively described in \cite{whelp}. Let us just recall here that -the whelp metadata model is essentially based a single ternary relation +the \WHELP metadata model is essentially based a single ternary relation \REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a given position $p$, where the position specify the place of the occurrence of $t$ inside $s$ (we currently work with a fixed set of @@ -787,18 +787,18 @@ A first, very simple but not negligeable feature is the check for duplicates. As soon as a new statement is defined, and before proving it, the library is searched to check that no other equivalent statement has been already proved -(based on the \whelp{} pattern matching functionality); if this is the case, +(based on the \WHELP pattern matching functionality); if this is the case, a warning is raised to the user. At present, the notion of equivalence adopted by Matita is convertibility, but we may imagine to weaken it in the future, covering for instance isomorphisms. -Another usefull \whelp{} operation is {\em hint}; we may invoke this query +Another usefull \WHELP operation is {\em hint}; we may invoke this query at any moment during the development of a proof, resulting in the list of all theorems of the library which can be applied to the current goal. In practice, this is mostly used not really to discover what theorems can be applied to a given goal, but to actually retrieve a theorem that we wish to apply, but whose name we have forgotten. -In fact, even if \Matita adopts a semi-rigid naming convention for +In fact, even if \MATITA adopts a semi-rigid naming convention for statements \ref{naming} that greatly simplifies the effort of recalling names, the naming discipline remains one of the most annoying aspects of formal developments, and the hint feature provides -- 2.39.2