X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Ftest.tex;h=057a1f54b1e9912f234acc58820c707fe401a5f5;hb=802e118337ebd0f8b732d4939973aae6415b5bec;hp=80f7656529477e372a0024146e84a3c074792abe;hpb=a961a1237063702ed9c32a9a4b7994671cb40818;p=helm.git

diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index 80f765652..057a1f54b 100644
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -6,11 +6,43 @@
 
 \begin{document}
 
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type}
 
 \bigskip
 
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body}
 
 \bigskip
 
@@ -20,6 +52,9 @@
 
 \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
 
+\bigskip
+
+\ObjRef{pr0}
 \ObjRef{pr0_ind}
 \ObjRef{pr0_confluence}