update in ground_2 and basic_2 (partial commit)

[helm.git] / matita / components / binaries / matex / test / test.tex

diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index 057a1f54b1e9912f234acc58820c707fe401a5f5..081696291d217993ab27e8d1ba56cf3361405a56 100644 (file)
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -1,61 +1,26 @@
-\documentclass[8pt,twocolumn]{extarticle}
+\documentclass[8pt,twocolumn,a4paper]{extarticle}
 
-\usepackage[bookmarks=false,ps2pdf]{hyperref}
+\usepackage[margin=2cm]{geometry}
+\usepackage[pdfborder={0 0 0},bookmarks=false,ps2pdf]{hyperref}
 \usepackage[american]{babel}
 \usepackage{matex}
+\usepackage{legacy_1}
+\usepackage{ground_1}
+\usepackage{basic_1}
 
-\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
+\newcounter{node}
+\renewcommand*\ObjIncNode{\stepcounter{node}}
+\renewcommand*\ObjNode{\arabic{node}}
 
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type}
+\title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$:
+Definitions and Statements}
 
-\bigskip
+\author{Ferruccio Guidi}
 
-\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
-
-\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\begin{document}
 
-\bigskip
+\maketitle
 
-\ObjRef{pr0}
-\ObjRef{pr0_ind}
-\ObjRef{pr0_confluence}
+\input{objs}
 
 \end{document}