X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_operational.tex;h=a7b3a9a49dcfcef733349d20dac34d854253ea74;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7868d3545744b105b808924dcb239bc9625d58d8;hpb=468da7af4b52d01451073ff1cca5aa1949b9657f;p=helm.git

diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex
index 7868d3545..a7b3a9a49 100644
--- a/helm/mathql/doc/mathql_operational.tex
+++ b/helm/mathql/doc/mathql_operational.tex
@@ -1,14 +1,14 @@
-\section {Operational semantics} \label {Operational}
+\section {Operational Semantics} \label {Operational}
 
 This section describes {\MathQL} semantics, that we present in a natural
 operational style \cite{Lan98,Win93}. 
 Here we use a simple type system that includes basic types such as strings and
 Booleans, and some type constructors such as product and exponentiation.
 $ y \oft Y $ will denote a typing judgement.
-Note that this semantics is not meant as a formal system \emph{per se}, but
-should serve as a reference for implementors.
+This semantics is not meant as a formal system \emph{per se}, but should be a
+reference for implementors.
 
 \input{mathql_operational_background}
 \input{mathql_operational_core}
-\input{mathql_operational_library}
+\input{mathql_operational_basic}