]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/doc/mathql_operational.tex
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / mathql / doc / mathql_operational.tex
diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex
deleted file mode 100644 (file)
index a7b3a9a..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-\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.
-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_basic}
-