X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Ftest.tex;h=057a1f54b1e9912f234acc58820c707fe401a5f5;hb=709537efda53c6189ed3e3e9877f1f93ac6d512a;hp=ddf18c40838abf537e74e295a431c646be81d9dc;hpb=21679cd1397d9c51519dbe439c29c1683b91ec64;p=helm.git diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index ddf18c408..057a1f54b 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -1,13 +1,61 @@ -\documentclass{article} +\documentclass[8pt,twocolumn]{extarticle} +\usepackage[bookmarks=false,ps2pdf]{hyperref} +\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} + +\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 +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} + +\bigskip -% \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} +\ObjRef{pr0} +\ObjRef{pr0_ind} +\ObjRef{pr0_confluence} \end{document}