X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fmain.tex;fp=helm%2Focaml%2Ftactics%2Fdoc%2Fmain.tex;h=06952d61cb3bf1e814c521fb9b7ff48bb6383392;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
new file mode 100644
index 000000000..06952d61c
--- /dev/null
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -0,0 +1,70 @@
+\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}
+