X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Ftest.tex;fp=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Ftest.tex;h=a85f8c8f6234112dcef1a32dfd9d0be9bd2ef392;hb=5791ee6b64136ecb0a727e32997b33f4bfab2c31;hp=057a1f54b1e9912f234acc58820c707fe401a5f5;hpb=709537efda53c6189ed3e3e9877f1f93ac6d512a;p=helm.git diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index 057a1f54b..a85f8c8f6 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -4,53 +4,13 @@ \usepackage[american]{babel} \usepackage{matex} -\begin{document} - -\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type} - -\bigskip - -\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} +\newcounter{node} +\renewcommand*\ObjIncNode{\stepcounter{node}} +\renewcommand*\ObjNode{\arabic{node} } -\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 - -\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type} - -\bigskip +\begin{document} -\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} +\input{objs} \bigskip