1 files changed, 75 insertions, 0 deletions
diff --git a/doc/RecTutorial/recmacros.tex b/doc/RecTutorial/recmacros.tex
new file mode 100644
index 00000000..0334553f
--- /dev/null
+++ b/doc/RecTutorial/recmacros.tex
@@ -0,0 +1,75 @@
+%===================================
+% 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}}
+
+
+%=======================================
+