\documentclass[a4]{seminar}
\usepackage{advi}
%\usepackage{advi-graphicx}
\usepackage[all]{xypic}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xypic}

\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}

\slideframe{none}
\newpagestyle{fw}{}{\hfil\blue{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\begin{slide}
\sectiontitle{mmode}
\slidetitle{a Mizar mode for Coq by Mariusz Giero}
$$\xymatrix{
{\begin{array}{c}\mbox{\advirecord{a}{\textbf{Coq}}\adviplay{a}} \vspace{-\smallskipamount}\\
\mbox{procedural proof}\end{array}}\adviwait &
{\begin{array}{c}\mbox{\textbf{Mizar}} \vspace{-\smallskipamount}\\
\mbox{\advirecord{b}{declarative proof}\adviplay{b}}\end{array}}\adviwait \\ \\
{\begin{array}{c}\mbox{\adviplay[slidered]{a}\adviplay[slidered]{b}\red{Mizar mode for Coq}} \vspace{-1.2\smallskipamount}\\
\advirecord{x}{\mbox{\llap{\green{{Henk}:}\quad}{{`mathematical mode'}}}} \vspace{-1.2\smallskipamount}\\
\advirecord{y}{\mbox{{`Mariusz' mode'}}} \\
\advirecord{z}{\mbox{{\textbf{mmode}}}}\end{array}}
\ar@{<-}[uu]^(.60){\mbox{\gray{everything else\ }}}
\ar@{<--}[uur]_(.68){\mbox{\gray{\ proof style}}}
}$$
\adviwait
\adviplay{x}
\adviwait
\adviplay{y}
%\adviwait
\adviplay{z}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{four mmode translations}
\begin{itemize}
\item[$\bullet$]
a basic Coq proof \\ \red{\texttt{Included\char`\_Add}}
\adviwait

\item[$\bullet$]
a complicated Coq proof from our C-CoRN library \\ \red{\texttt{FTA'}}
\adviwait

own tactics: \green{\texttt{Algebra}}, \green{\texttt{Rational}}
\adviwait

\item[$\bullet$]
a basic Mizar proof \\ \red{\texttt{min\char`\_przerobka\char`\_2}} \adviwait
$$\min(x,y) = {x + y - |x - y|\over 2}
\vspace{-\bigskipamount}
$$
\adviwait

\item[$\bullet$]
one of Henk's `mathematical mode' experiments \\ \red{\texttt{nat\char`\_factorizes}}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{trying to keep it as simple to use as possible}
\blue{our goal:} just say
\begin{center}
\red{\texttt{Require mmode.}}
\end{center}
%at the start of your file
\adviwait
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{no special parser} \\
\advirecord{p}{can't use existing Coq keywords: \green{\texttt{LEt}}/\green{\texttt{MLet}}, \green{\texttt{MShow}}}

%\gray{Mizar Light mode for HOL} \\
\red{just a bunch of Coq tactics}
\adviwait
\adviplay[slidegreen]{p}
\adviwait

\item[$\bullet$]
\textbf{only ${\cal L}_{\rm tac}$ tactics} \\
\advirecord{q}{currently uses one ML level tactic: \texttt{Msg}}

no ML level tactics\quad $\to$\quad no need for a special image %to run it natively
\adviwait
\adviplay[slidegreen]{q}
\adviwait
\medskip

\item[$\bullet$]
\textbf{\green{needs a patch to Coq 7.4}} \\
\gray{`tactics that take tactics as arguments'}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{work in progress}
\bigskip
\bigskip

\begin{center}
\textbf{demo}
\end{center}

\vfill
\end{slide}

\end{document}