X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Flegacy_1.sty;fp=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Flegacy_1.sty;h=10edd9b625af3d1743705afae2bf302c68ea8e2f;hb=e06774421eb3b8f4438a6876cc1ab4262ef16f6e;hp=d33196fb2b62be5c1c398ff79fba886f2b0ebd44;hpb=b4b18a8f2c3f33fe49edef3bc8068332edf299e2;p=helm.git

diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty
index d33196fb2..10edd9b62 100644
--- a/matita/components/binaries/matex/test/legacy_1.sty
+++ b/matita/components/binaries/matex/test/legacy_1.sty
@@ -1,10 +1,42 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{lambdadelta_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\ProvidesPackage{legacy_1}[2016/06/06 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\RequirePackage{matex}
+\RequirePackage{fdsymbol}
 \ExecuteOptions{}
 \ProcessOptions*
 
+\let\OldSucc=\Succ
+
 \makeatletter
 
+\newcommand*\ld@and[1]{\setbinlink{\&}{#1}}
+\newcommand*\ld@lex[1]{\setordlink{\exists}{#1}}
+\newcommand*\ld@land[1]{\setrellink{\land}{#1}}
+\newcommand*\ld@lor[1]{\setrellink{\lor}{#1}}
+
+\newcommand*\ld@eq[1]{\setrellink{=}{#1}}
+\newcommand*\ld@le[1]{\setrellink{\le}{#1}}
+\newcommand*\ld@lt[1]{\setrellink{<}{#1}}
+\newcommand*\ld@minus[1]{\setbinlink{+}{#1}}
+\newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}}
+\newcommand*\ld@plus[1]{\setbinlink{-}{#1}}
+\newcommand*\ld@pred[1]{\setoplink{\downspoon}{#1}}
+\newcommand*\ld@succ[1]{\setoplink{\upspoon}{#1}}
+
+\newcommand*\LAndB[3]{#2\ld@land{#1}#3}
+\newcommand*\LOrB[3]{#2\ld@lor{#1}#3}
+\newcommand*\LExAA[3]{\ld@lex{#1}#3}
+\newcommand*\LExBA[4]{\ld@lex{#1}#3\ld@and{#1}#4}
+
+\newcommand*\EQ[4]{#3\ld@eq{#1}#4}
+\newcommand*\LE[3]{#2\ld@le{#1}#3}
+\newcommand*\LT[3]{#2\ld@lt{#1}#3}
+\newcommand*\Minus[3]{#2\ld@minus{#1}#3}
+\newcommand*\LNot[2]{\ld@lnot{#1}#2}
+\newcommand*\Plus[3]{#2\ld@plus{#1}#3}
+\newcommand*\Pred[2]{\ld@pred{#1}#2}
+\renewcommand*\Succ[2]{\ld@succ{#1}#2}
+
 \makeatother
 
 \endinput