]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/doc/mathql_operational.tex
updating all sections
[helm.git] / helm / mathql / doc / mathql_operational.tex
index 7868d3545744b105b808924dcb239bc9625d58d8..32be697a50486a2ac4b99142a91c26613e9ccba4 100644 (file)
@@ -5,10 +5,10 @@ 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}