- renamed ocaml/ to components/

[helm.git] / helm / ocaml / tactics / doc / main.tex

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
deleted file mode 100644 (file)
index 06952d6..0000000
--- a/helm/ocaml/tactics/doc/main.tex
+++ /dev/null
@@ -1,70 +0,0 @@
-\documentclass[a4paper]{article}
-
-\usepackage{a4wide}
-\usepackage{pifont}
-\usepackage{semantic}
-\usepackage{stmaryrd}
-\usepackage{graphicx}
-
-\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
-
-\title{Continuationals semantics for \MATITA}
-\author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
-\small Department of Computer Science, University of Bologna \\
-\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
-\small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
-
-\newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
-\newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}
-
-\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
-\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
-\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
-\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
-\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
-\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
-\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
-\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
-\newcommand{\SKIP}{\MATHTT{skip}}
-\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
-
-\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
-
-\newcommand{\GOAL}{\MATHIT{goal}}
-\newcommand{\SWITCH}{\MATHIT{switch}}
-\newcommand{\LIST}{\MATHTT{list}}
-\newcommand{\INT}{\MATHTT{int}}
-\newcommand{\OPEN}{\MATHTT{Open}}
-\newcommand{\CLOSED}{\MATHTT{Closed}}
-
-\newcommand{\SEMOP}[1]{|[#1|]}
-\newcommand{\TSEMOP}[1]{{}_t|[#1|]}
-\newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
-\newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
-\newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
-
-\newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}}
-
-\newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
-\newcommand{\INITPOS}{\MATHIT{init\_pos}}
-\newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
-\newcommand{\FILTER}{\MATHIT{filter}}
-\newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
-\newcommand{\ISOPEN}{\MATHIT{is\_open}}
-\newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
-\newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
-\newcommand{\GOALS}{\MATHIT{open\_goals}}
-
-\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
-\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}
-
-\newlength{\sidecondlen}
-\setlength{\sidecondlen}{2cm}
-
-\begin{document}
-\maketitle
-
-\input{body.tex}
-
-\end{document}
-