]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/matex/test/test.tex
- ground_2: support for relocation updated
[helm.git] / matita / components / binaries / matex / test / test.tex
index ddf18c40838abf537e74e295a431c646be81d9dc..057a1f54b1e9912f234acc58820c707fe401a5f5 100644 (file)
@@ -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}