1 files changed, 0 insertions, 75 deletions
diff --git a/doc/RecTutorial/recmacros.tex b/doc/RecTutorial/recmacros.tex
deleted file mode 100644
index 0334553f2..000000000
--- a/doc/RecTutorial/recmacros.tex
+++ /dev/null
@@ -1,75 +0,0 @@
-%===================================
-% Style of the document
-%===================================
-%\newtheorem{example}{Example}[section]
-%\newtheorem{exercise}{Exercise}[section]
-
-
-\newcommand{\comentario}[1]{\texttt{#1}}
-
-%===================================
-% Keywords
-%===================================
-
-\newcommand{\Prop}{\texttt{Prop}}
-\newcommand{\Set}{\texttt{Set}}
-\newcommand{\Type}{\texttt{Type}}
-\newcommand{\true}{\texttt{true}}
-\newcommand{\false}{\texttt{false}}
-\newcommand{\Lth}{\texttt{Lth}}
-
-\newcommand{\Nat}{\texttt{nat}}
-\newcommand{\nat}{\texttt{nat}}
-\newcommand{\Z}  {\texttt{O}}
-\newcommand{\SUCC}{\texttt{S}}
-\newcommand{\pred}{\texttt{pred}}
-
-\newcommand{\False}{\texttt{False}}
-\newcommand{\True}{\texttt{True}}
-\newcommand{\I}{\texttt{I}}
-
-\newcommand{\natind}{\texttt{nat\_ind}}
-\newcommand{\natrec}{\texttt{nat\_rec}}
-\newcommand{\natrect}{\texttt{nat\_rect}}
-
-\newcommand{\eqT}{\texttt{eqT}}
-\newcommand{\identityT}{\texttt{identityT}}
-
-\newcommand{\map}{\texttt{map}}
-\newcommand{\iterates}{\texttt{iterates}}
-
-
-%===================================
-% Numbering
-%===================================
-
-
-\newtheorem{definition}{Definition}[section]
-\newtheorem{example}{Example}[section]
-
-
-%===================================
-% Judgements 
-%===================================
-
-
-\newcommand{\JM}[2]{\ensuremath{#1 : #2}}
-
-%===================================
-% Expressions 
-%===================================
-
-\newcommand{\Case}[3][]{\ensuremath{#1\textsf{Case}~#2~\textsf of}~#3~\textsf{end}}
-
-%=======================================
-
-\newcommand{\snreglados} [3] {\begin{tabular}{c} \ensuremath{#1} \\[2pt]
-   \ensuremath{#2}\\ \hline  \ensuremath{#3}  \end{tabular}}
-
-
-\newcommand{\snregla} [2] {\begin{tabular}{c}
-   \ensuremath{#1}\\ \hline  \ensuremath{#2}  \end{tabular}}
-
-
-%=======================================
-