X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fmatex.sty;h=505d68176b7ad466449aa3bf7502cf25f33afa75;hb=788e7cb15734fd228e8788ea628934af483ae772;hp=0312b6d1d30707718c66154afed2af1eebc1b117;hpb=2ffd7e47f1872878f6af4084074655da5cf3b23e;p=helm.git

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 0312b6d1d..505d68176 100644
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,12 +1,51 @@
-\newcommand*\Next[1]{\def\TMP{#1}\ifx\TMP\empty\let\next=\relax\else\ #1\let\next=\Next\fi\next}
-
-\newcommand*\Prop{PROP}
-\newcommand*\Crop[1]{CROP}
-\newcommand*\Type[1]{TYPE}
-\newcommand*\LRef[1]{(L #1)}
-\newcommand*\GRef{G}
-\newcommand*\Abbr[3]{(D #1 #2 #3) }
-\newcommand*\Abst[2]{(I #1 #2) }
-\newcommand*\Prod[2]{(P #1 #2) }
-\newcommand*\Appl{(A)\Next}
-\newcommand*\Case[3]{(C #1 #2 #3)\Next}
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{matex}[2015/12/21 MaTeX Package]
+\ExecuteOptions{}
+\ProcessOptions*
+
+\makeatletter
+
+\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+
+\newcommand*\ObjLabel[1]{\label{obj:#1}}
+\newcommand*\ObjRef[1]{\ref{obj:#1}}
+
+\newtheorem{prop}{Proposition}
+\newenvironment{proof}{\setlength\parindent{0pt}}{}
+\newenvironment{ma@step}{}{\vskip0pt}
+
+\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+
+\newcommand*\ma@tmp{}
+\newcommand*\ma@skip[4]{}
+\newcommand*\ma@next[5]{\def\ma@tmp{#5}\ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi\ma@tmp #3#2#3#4}
+
+\newcommand*\ma@space{ }
+\newcommand*\ma@arg[1]{#1}
+
+\newcommand*\PROP{PROP}
+\newcommand*\CROP[1]{CROP}
+\newcommand*\TYPE[1]{TYPE}
+\newcommand*\LREF[2]{#1}
+\newcommand*\GREF[2]{#1}
+\newcommand*\ABBR[3]{(D #1 #2 #3) }
+\newcommand*\ABST[2]{(I #1 #2) }
+\newcommand*\PROD[2]{(P #1 #2) }
+\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
+\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
+
+\newcommand*\ma@with{ with }
+\newcommand*\ma@comma{, }
+\newcommand*\ma@stop{.\end{ma@step}}
+
+\newcommand*\DECL[3]{\def\ma@tmp{#1}\begin{ma@step}\textbf{\ifx\ma@tmp\empty\_conlusion\else #1\fi} of type #3}
+\newcommand*\PRIM{\end{ma@step}}
+\newcommand*\BODY[1]{\\is #1\end{ma@step}}
+\newcommand*\STEP[1]{\\by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\DEST[1]{\\by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\OPEN[3]{\begin{ma@step}\textbf{#1} is the following scope #3.\end{ma@step}}
+\newcommand*\EXIT[1]{\begin{ma@step}\textbf{end} of scope #1.\end{ma@step}}
+
+\makeatother
+
+\endinput