]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/doc/main.tex
Reshaped structure of ocaml/ libraries.
[helm.git] / helm / ocaml / cic_notation / doc / main.tex
diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
deleted file mode 100644 (file)
index 36d3502..0000000
+++ /dev/null
@@ -1,43 +0,0 @@
-\documentclass[a4paper,draft]{article}
-
-\usepackage{manfnt}
-\usepackage{a4wide}
-\usepackage{pifont}
-\usepackage{semantic}
-\usepackage{stmaryrd,latexsym}
-
-\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
-
-\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
-
-\title{Extensible notation for \MATITA}
-\author{Luca Padovani \qquad Stefano Zacchiroli \\
-\small Department of Computer Science, University of Bologna \\
-\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
-\small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
-
-\newcommand{\BREAK}{\mathtt{break}}
-\newcommand{\TVAR}[1]{#1:\mathtt{term}}
-\newcommand{\IMPVAR}{\TVAR{\_}}
-\newcommand{\NVAR}[1]{#1:\mathtt{number}}
-\newcommand{\IVAR}[1]{#1:\mathtt{name}}
-\newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
-\newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
-\newcommand{\IOT}[2]{|[#1|]_{#2}^2}
-\newcommand{\IAP}[2]{|[#1|]_{#2}^a}
-\newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a}
-\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
-\newcommand{\NAMES}{\mathit{names}}
-\newcommand{\DOMAIN}{\mathit{domain}}
-\newcommand{\UPDATE}[2]{#1[#2]}
-
-\mathlig{~>}{\leadsto}
-\mathlig{|->}{\mapsto}
-
-\begin{document}
-  \maketitle
-
-  \input{body}
-
-\end{document}
-