From 804b1a97072cf1d1c76bc32338d0b068bcb2159f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 6 Dec 2005 11:57:34 +0000 Subject: [PATCH] Minor changes. --- 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 2cc1dc8a0..fad520ad3 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1287,9 +1287,9 @@ symmetric property for relations Then, you may state the symmetry of equality as \[ \forall A:Type. symmetric \;A\;(eq \; A)\] -and \verb+symmetric_eq+ is valid Matita name fo such a theorem. +and \verb+symmetric_eq+ is valid Matita name for such a theorem. So, somehow unexpectedly, the introduction of semi-rigid naming convention -also had benefical effects on the global organization of the library, +has an important benefical effect on the global organization of the library, forcing the user to define abstract notions and properties before using them (and formalizing such use). @@ -1313,11 +1313,11 @@ A typical example is the following \end{verbatim} where $eqb$ is boolean equality. In this cases, the name can be build starting from the matched -expression and the suffix $_to_Prop$. In the above example, -$eqb_to_Prop$ is accepted. - +expression and the suffix \verb+_to_Prop+. In the above example, +\verb+eqb_to_Prop+ is accepted. +\section{Conclusions} \acknowledgements We would like to thank all the students that during the past -- 2.39.2