- matex: we separate axioms (propositions) and assumptions (other)

- matex.sty: some improvements including
                  color for metalinguistic term constructions
- stylesheets: some improvements including more notation for basic_1

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 83de453f733993275e73d7024a037015b8e3fc77..c3d50d5e74fdd4bf2c8a5e481b11d3f50a08e67d 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -262,10 +262,14 @@ let open_out_tex s =
    open_out (F.concat !G.out_dir fname)
 
 let proc_pair s ss u = function
-   | None   -> 
+   | None   ->
+      let text_u =
+         if K.not_prop1 [] u then proc_item "assumption"
+         else proc_item "axiom" 
+      in
       let name = X.rev_map_concat X.id "." "type" ss in
       let och = open_out_tex name in
-         O.out_text och (proc_item "axiom" s name u);
+         O.out_text och (text_u s name u);
       close_out och
    | Some t ->
       let text_u, text_t =

diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml
index 451e77ba5039dc547ef0524f2c89e3845ddae1d2..10095057bb45b09ad21802e6bacd81fb6afc1aa2 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.conf.xml
+++ b/matita/components/binaries/matex/test/basic_1.conf.xml
@@ -174,76 +174,58 @@
     <key name="const">$(devel.basic1).A.defs.A.ASort.type AtomB 2 0</key>
 <!--
 $(devel.basic1).A.fwd.A_rect.A_rect.type 0</key>
-$(devel.basic1).aplus.defs.aplus.aplus.type 0</key>
 -->
+    <key name="const">$(devel.basic1).aplus.defs.aplus.aplus.type PlusA 3 0</key>
     <key name="const">$(devel.basic1).app.defs.app1.app1.type Shift 2 0</key>
     <key name="const">$(devel.basic1).app.defs.cbk.cbk.type Level 1 0</key>
-<!--
-$(devel.basic1).aprem.defs.aprem.aprem.type 0</key>
--->
+    <key name="const">$(devel.basic1).aprem.defs.aprem.aprem.type CoPremise 3 0</key>
     <key name="const">$(devel.basic1).arity.defs.arity.arity.type Arity 4 0</key>
-<!--
-$(devel.basic1).asucc.defs.asucc.asucc.type 0</key>
-$(devel.basic1).C.defs.C.CHead.type 0</key>
--->
+    <key name="const">$(devel.basic1).asucc.defs.asucc.asucc.type SuccA 2 0</key>
+    <key name="const">$(devel.basic1).C.defs.C.CHead.type LHead 3 0</key>
     <key name="const">$(devel.basic1).C.defs.C.CSort.type AtomA 1 0</key>
     <key name="const">$(devel.basic1).C.defs.cle.type LE 2 0</key>
     <key name="const">$(devel.basic1).C.defs.clt.type LT 2 0</key>
-<!--
-$(devel.basic1).C.defs.CTail.CTail.type 0</key>
--->
+    <key name="const">$(devel.basic1).C.defs.CTail.CTail.type THead 3 0</key>
     <key name="const">$(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0</key>
 <!--
 $(devel.basic1).C.fwd.C_rect.C_rect.type 0</key>
-$(devel.basic1).cimp.defs.cimp.type 0</key>
 -->
+    <key name="const">$(devel.basic1).cimp.defs.cimp.type SubEq 2 0</key>
     <key name="const">$(devel.basic1).clear.defs.clear.clear.type Drop 2 0</key>
     <key name="const">$(devel.basic1).clen.defs.clen.clen.type Length 1 0</key>
     <key name="const">$(devel.basic1).cnt.defs.cnt.cnt.type LEnv 1 0</key>
-<!--
-$(devel.basic1).csuba.defs.csuba.csuba.type 0</key>
-$(devel.basic1).csubc.defs.csubc.csubc.type 0</key>
--->
+    <key name="const">$(devel.basic1).csuba.defs.csuba.csuba.type LSupA 3 0</key>
+    <key name="const">$(devel.basic1).csubc.defs.csubc.csubc.type LSupC 3 0</key>
     <key name="const">$(devel.basic1).csubst0.defs.csubst0.csubst0.type Subst 4 0</key>
     <key name="const">$(devel.basic1).csubst1.defs.csubst1.csubst1.type SubstS 4 0</key>
-<!--
-$(devel.basic1).csubt.defs.csubt.csubt.type 0</key>
-$(devel.basic1).csubv.defs.csubv.csubv.type 0</key>
--->
+    <key name="const">$(devel.basic1).csubt.defs.csubt.csubt.type LSupT 3 0</key>
+    <key name="const">$(devel.basic1).csubv.defs.csubv.csubv.type LSup 2 0</key>
     <key name="const">$(devel.basic1).drop1.defs.drop1.drop1.type DropS 3 0</key>
-<!--
-$(devel.basic1).drop1.defs.ptrans.ptrans.type 0</key>
--->
+    <key name="const">$(devel.basic1).drop1.defs.ptrans.ptrans.type ApplS 2 0</key>
     <key name="const">$(devel.basic1).drop.defs.drop.drop.type DropB 4 0</key>
     <key name="const">$(devel.basic1).ex0.defs.leqz.leqz.type Equiv 2 0</key>
     <key name="const">$(devel.basic1).flt.defs.flt.type LTB 4 0</key>
     <key name="const">$(devel.basic1).flt.defs.fweight.type WeightB 2 0</key>
     <key name="const">$(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type SubstB 6 0</key>
-<!--
-$(devel.basic1).G.defs.G.mk_G.type 0</key>
--->
+    <key name="const">$(devel.basic1).G.defs.G.mk_G.type MkSH 2 0</key>
     <key name="const">$(devel.basic1).G.defs.next.next.type Next 2 0</key>
     <key name="const">$(devel.basic1).getl.defs.getl.getl.type DropA 3 0</key>
     <key name="const">$(devel.basic1).iso.defs.iso.iso.type SameTop 2 0</key>
     <key name="const">$(devel.basic1).leq.defs.leq.leq.type EquivA 3 0</key>
     <key name="const">$(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0</key>
     <key name="const">$(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0</key>
-<!--
-$(devel.basic1).lift1.defs.trans.trans.type 0</key>
--->
+    <key name="const">$(devel.basic1).lift1.defs.trans.trans.type Appl 2 0</key>
     <key name="const">$(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0</key>
     <key name="const">$(devel.basic1).lift.defs.lift.type FunLift 3 0</key>
     <key name="const">$(devel.basic1).lift.defs.lref_map.lref_map.type FunLift 3 0</key>
     <key name="const">$(devel.basic1).llt.defs.llt.type LT 2 0</key>
     <key name="const">$(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0</key>
-<!--
-$(devel.basic1).next_plus.defs.next_plus.next_plus.type 0</key>
--->
+    <key name="const">$(devel.basic1).next_plus.defs.next_plus.next_plus.type NextS 3 0</key>
     <key name="const">$(devel.basic1).nf2.defs.nf2.type RNormal 2 0</key>
     <key name="const">$(devel.basic1).nf2.defs.nfs2.nfs2.type RNormal 2 0</key>
-    <key name="const">$(devel.basic1).pc1.defs.pc1.type Convert 3 0</key>
-    <key name="const">$(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertS 3 0</key>
-    <key name="const">$(devel.basic1).pc3.defs.pc3.type ConvertS 3 0</key>
+    <key name="const">$(devel.basic1).pc1.defs.pc1.type ConvertS 2 0</key>
+    <key name="const">$(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertSA 3 0</key>
+    <key name="const">$(devel.basic1).pc3.defs.pc3.type ConvertSA 3 0</key>
     <key name="const">$(devel.basic1).pr0.defs.pr0.pr0.type RStep 2 0</key>
     <key name="const">$(devel.basic1).pr1.defs.pr1.pr1.type RStepS 2 0</key>
     <key name="const">$(devel.basic1).pr2.defs.pr2.pr2.type RStepA 3 0</key>
@@ -258,14 +240,10 @@ $(devel.basic1).next_plus.defs.next_plus.next_plus.type 0</key>
     <key name="const">$(devel.basic1).subst0.defs.subst0.subst0.type Subst 4 0</key>
     <key name="const">$(devel.basic1).subst1.defs.subst1.subst1.type SubstS 4 0</key>
     <key name="const">$(devel.basic1).subst.defs.subst.subst.type FunSubstS 3 0</key>
-<!--
-$(devel.basic1).T.defs.K.Bind.type 0</key>
-$(devel.basic1).T.defs.K.Flat.type 0</key>
--->
+    <key name="const">$(devel.basic1).T.defs.K.Bind.type Bind 1 0</key>
+    <key name="const">$(devel.basic1).T.defs.K.Flat.type Flat 1 0</key>
     <key name="const">$(devel.basic1).T.defs.tle.type LE 2 0</key>
-<!--
-$(devel.basic1).T.defs.T.THead.type 0</key>
--->
+    <key name="const">$(devel.basic1).T.defs.T.THead.type THead 3 0</key>
     <key name="const">$(devel.basic1).T.defs.T.TLRef.type LRef 1 0</key>
     <key name="const">$(devel.basic1).T.defs.T.TSort.type AtomA 1 0</key>
     <key name="const">$(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0</key>
@@ -273,9 +251,7 @@ $(devel.basic1).T.defs.T.THead.type 0</key>
 $(devel.basic1).T.fwd.T_rect.T_rect.type 0</key>
 -->
     <key name="const">$(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0</key>
-<!--
-$(devel.basic1).tlist.defs.THeads.THeads.type 0</key>
--->
+    <key name="const">$(devel.basic1).tlist.defs.THeads.THeads.type THead 3 0</key>
     <key name="const">$(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0</key>
     <key name="const">$(devel.basic1).tlist.defs.tslen.tslen.type Length 1 0</key>
     <key name="const">$(devel.basic1).tlist.defs.tslt.type LT 2 0</key>

diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty
index 27fbe98b29370931511c09205003976f53224640..71e48ff0235dcb3606f19b036d708011065573bd 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.sty
+++ b/matita/components/binaries/matex/test/basic_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{basic_1}[2016/06/24 Notation for "cic:/matita/lambdadelta/basic_1/"]
+\ProvidesPackage{basic_1}[2016/07/03 Notation for "cic:/matita/lambdadelta/basic_1/"]
 \RequirePackage{legacy_1}
 \RequirePackage{ground_1}
 \ExecuteOptions{}
@@ -14,19 +14,25 @@
 \newcommand*\ld@oB[1]{\mathopen{\lBrack}}
 \newcommand*\ld@cB[1]{\mathopen{\rBrack}}
 \newcommand*\ld@env[1]{\mathrel{\vdash}}
+\newcommand*\ld@fs[1]{\mathord{.}}
 
+\newcommand*\ld@appl[1]{\setbinlink{@}{#1}{}}
+\newcommand*\ld@appls[1]{\setbinlink{\overline{@}}{#1}{}}
 \newcommand*\ld@arity[2]{\setrellink{\mathsf{arity}}{#1}{#2}}
+\newcommand*\ld@bind[1]{\setordlink{\mathbf{B}}{#1}{}}
 \newcommand*\ld@coconverts[1]{\setrellink{\mathsf{convert}_{\mathord\oplusrhrim}^*}{#1}{}}
-\newcommand*\ld@convert[1]{\setrellink{\mathsf{convert}}{#1}{}}
 \newcommand*\ld@converts[1]{\setrellink{\mathsf{convert}^*}{#1}{}}
+\newcommand*\ld@copremise[2]{\setoplink{\mathsf{copremise}}{#1}{#2}}
 \newcommand*\ld@coweight[1]{\setoplink{\equivVvert}{#1}{}}
 \newcommand*\ld@drop[2]{\setoplink{\Downarrow}{#1}{#2}}
 \newcommand*\ld@drops[2]{\setoplink{\Downarrow^*}{#1}{#2}}
 \newcommand*\ld@equiv[2]{\setrellink{\equiv}{#1}{#2}}
+\newcommand*\ld@flat[1]{\setoplink{\mathbf{F}}{#1}{}}
 \newcommand*\ld@funlift[2]{\setoplink{\uparrow}{#1}{#2}}
-\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{}}
+\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{#2}}
 \newcommand*\ld@funv[2]{\setoplink{\mathsf{v}}{#1}{#2}}
 \newcommand*\ld@funw[2]{\setoplink{\mathsf{w}}{#1}{#2}}
+\newcommand*\ld@pair[2]{\setordlink{\mathbf{P}}{#1}{#2}}
 \newcommand*\ld@in[1]{\setrellink{\in}{#1}{}}
 \newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}}
 \newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}}
@@ -34,6 +40,10 @@
 \newcommand*\ld@lenv[1]{\setoplink{\mathsf{lenv}}{#1}{}}
 \newcommand*\ld@level[1]{\setoplink{\mathsf{level}}{#1}{}}
 \newcommand*\ld@lref[1]{\setoplink{\#}{#1}{}}
+\newcommand*\ld@lsup[2]{\setrellink{\sqsupseteq}{#1}{#2}}
+\newcommand*\ld@lsupa[2]{\setrellink{\mathord\sqsupseteq\lozenge}{#1}{#2}}
+\newcommand*\ld@lsupt[2]{\setrellink{\mathord\sqsupseteq\mathord:}{#1}{#2}}
+\newcommand*\ld@mksh[1]{\setordlink{\mathbf{H}}{#1}{}}
 \newcommand*\ld@next[2]{\setoplink{\mathsf{next}}{#1}{#2}}
 \newcommand*\ld@rcandidate[2]{\setoplink{\mathsf{r\_candidate}}{#1}{#2}}
 \newcommand*\ld@rnormal[1]{\setoplink{\mathsf{r\_normal}}{#1}{}}
@@ -42,6 +52,7 @@
 \newcommand*\ld@rstrong[1]{\setoplink{\mathsf{r\_strong}}{#1}{}}
 \newcommand*\ld@sametop[1]{\setrellink{\eqsim}{#1}{}}
 \newcommand*\ld@shift[1]{\setordlink{.}{#1}}
+\newcommand*\ld@subeq[1]{\setrellink{\subseteq}{#1}{}}
 \newcommand*\ld@subst[1]{\setbinlink{/}{#1}{}}
 \newcommand*\ld@substs[1]{\setbinlink{/^*}{#1}{}}
 \newcommand*\ld@to[1]{\setrellink{\rightarrow}{#1}{}}
@@ -53,14 +64,18 @@
 
 \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}}
 
+\newcommand*\Appl[3]{#2\ld@appl{#1}#3}
+\newcommand*\ApplS[3]{#2\ld@appls{#1}#3}
 \newcommand*\Arity[5]{#3\ld@env{#1}#4\ld@arity{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\AtomA[2]{\ld@leaf{#1}#2}
 \newcommand*\AtomB[3]{\ld@leaf{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\Bind[2]{\ld@bind{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\CoConsA[3]{#2\ld@cocons{#1}#3}
-\newcommand*\CoConvertS[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
+\newcommand*\CoConvertSA[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
 \newcommand*\ConsA[3]{#2\ld@cons{#1}#3}
-\newcommand*\Convert[4]{#2\ld@env{#1}#3\ld@convert{#1}#4}
-\newcommand*\ConvertS[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
+\newcommand*\ConvertS[3]{#2\ld@converts{#1}#3}
+\newcommand*\ConvertSA[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
+\newcommand*\CoPremise[4]{\ld@copremise{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 \newcommand*\CoWeightA[2]{\ld@coweight{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\CoWeightB[3]{\ld@coweight{#1}\ld@tuple@b{#1}{#2}{#3}}
 \newcommand*\Drop[3]{\ld@drop{#1}{}#2\ld@eq{#1}#3}
@@ -69,6 +84,7 @@
 \newcommand*\DropS[4]{\ld@drops{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 \renewcommand*\Equiv[3]{#2\ld@equiv{#1}{}#3}
 \newcommand*\EquivA[4]{#3\ld@equiv{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\Flat[2]{\ld@flat{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\FunLift[4]{\ld@funlift{#1}{\ld@tuple@b{#1}{#2}{#3}}#4}
 \newcommand*\FunLiftS[3]{\ld@funlifts{#1}{\ld@tuple@a{#1}{#2}}#3}
 \newcommand*\FunSubstS[4]{\mathop{\ld@ob{#1}#3\ld@substs{#1}#2\ld@cb{#1}}#4}
@@ -77,9 +93,17 @@
 \newcommand*\LEnv[2]{\ld@lenv{#1}#2}
 \newcommand*\Length[2]{\ld@length@open{#1}#2\ld@length@close{#1}}
 \newcommand*\Level[2]{\ld@level{#1}#2}
+\newcommand*\LHead[4]{#2\ld@fs{#1}\ld@pair{#1}{\ld@tuple@a{#1}{#3}}#4}
 \newcommand*\LRef[2]{\ld@lref{#1}#2}
+\newcommand*\LSup[3]{#2\ld@lsup{#1}{}#3}
+\newcommand*\LSupA[4]{#3\ld@lsupa{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupC[4]{#3\ld@lsup{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupT[4]{#3\ld@lsupt{#1}{\ld@tuple@a{#1}{#2}}#4}
 \newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}}
+\newcommand*\MkSH[3]{\ld@mksh{#1}\ld@tuple@b{#1}{#2}{#3}}
 \newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\NextS[4]{\ld@next{#1}{^{#4}\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\PlusA[4]{#3\ld@plus{#1}{\ld@tuple@a{#1}{#2}}#4}
 \newcommand*\RCandidate[5]{\ld@tuple@b{#1}{#3}{#4}\ld@in{#1}\ld@rcandidate{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\RNormal[3]{#2\ld@env{#1}\ld@rnormal{#1}#3}
 \newcommand*\RStep[3]{#2\ld@rstep{#1}#3}
@@ -89,9 +113,12 @@
 \newcommand*\RStrong[3]{#2\ld@env{#1}\ld@rstrong{#1}#3}
 \newcommand*\SameTop[3]{#2\ld@sametop{#1}#3}
 \newcommand*\Shift[3]{#2\ld@shift{#1}#3}
+\newcommand*\SubEq[3]{#2\ld@subeq{#1}#3}
 \newcommand*\Subst[5]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
 \newcommand*\SubstB[7]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}\ld@tuple@b{#1}{#4}{#5}\ld@eq{#1}\ld@tuple@b{#1}{#6}{#7}}
 \newcommand*\SubstS[5]{\mathop{\ld@oB{#1}#3\ld@substs{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\SuccA[3]{\ld@succ{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\THead[4]{\ld@pair{#1}{\ld@tuple@a{#1}{#2}}#3\ld@fs{#1}#4}
 \newcommand*\To[3]{#2\ld@to{#1}#3}
 \newcommand*\TStep[5]{#3\ld@env{#1}#4\ld@tstep{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\TStepS[5]{#3\ld@env{#1}#4\ld@tsteps{#1}{\ld@tuple@a{#1}{#2}}#5}

diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty
index f7dd9382b603ac252500165b99eb41910008c8ac..b240c44b170d4eb155742e459da9ae5432dee5f9 100644 (file)
--- a/matita/components/binaries/matex/test/legacy_1.sty
+++ b/matita/components/binaries/matex/test/legacy_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{legacy_1}[2016/06/21 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\ProvidesPackage{legacy_1}[2016/07/03 Notation for "cic:/matita/lambdadelta/legacy_1/"]
 \RequirePackage{matex}
 \ExecuteOptions{}
 \ProcessOptions*
@@ -18,9 +18,9 @@
 \newcommand*\ld@lt[1]{\setrellink{<}{#1}{}}
 \newcommand*\ld@minus[1]{\setbinlink{-}{#1}{}}
 \newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}{}}
-\newcommand*\ld@plus[1]{\setbinlink{+}{#1}{}}
+\newcommand*\ld@plus[2]{\setbinlink{+}{#1}{#2}}
 \newcommand*\ld@pred[1]{\setoplink{\midcir}{#1}{}}
-\newcommand*\ld@succ[1]{\setoplink{\cirmid}{#1}{}}
+\newcommand*\ld@succ[2]{\setoplink{\cirmid}{#1}{#2}}
 
 \newcommand*\ld@list[2]{\ma@list\relax\ma@arg{#1{#2}}\relax}
 
@@ -33,9 +33,9 @@
 \newcommand*\LT[3]{#2\ld@lt{#1}#3}
 \newcommand*\Minus[3]{#2\ld@minus{#1}#3}
 \newcommand*\LNot[2]{\ld@lnot{#1}#2}
-\newcommand*\Plus[3]{#2\ld@plus{#1}#3}
+\newcommand*\Plus[3]{#2\ld@plus{#1}{}#3}
 \newcommand*\Pred[2]{\ld@pred{#1}#2}
-\renewcommand*\Succ[2]{\ld@succ{#1}#2}
+\renewcommand*\Succ[2]{\ld@succ{#1}{}#2}
 
 \makeatother
 

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index b01223fefec60774fc182dabebde22033d01edea..7d6ae277e8b678f41181428b31e309b2ab5a6a1e 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,33 +1,43 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/06/21 MaTeX Package]
+\ProvidesPackage{matex}[2016/07/03 MaTeX Package]
 \RequirePackage{xcolor}
 \RequirePackage[lcgreekalpha]{stix}
 \ExecuteOptions{}
 \ProcessOptions*
 
-\makeatletter
+\newcommand*\neverindent{\setlength\parindent{0pt}}
 
-\newcommand*\ma@cast{\mathbin:}
-\newcommand*\ma@abbr{\mathrel\eqdef}
-\newcommand*\ma@prod{\mathord\Pi}
-\newcommand*\ma@arrw{\mathrel\Rightarrow}
-\newcommand*\ma@fall{\mathord\forall}
-\newcommand*\ma@impl{\mathrel\supset}
-\newcommand*\ma@case{\mathrel\questeq}
-\newcommand*\ma@caze{\mathrel\mapsto}
-\newcommand*\ma@pair{\mathbin\mapsto}
+\makeatletter
 
 \definecolor{ma@black}{HTML}{000000}
 \definecolor{ma@blue}{HTML}{00005F}
 \definecolor{ma@purple}{HTML}{3F005F}
+\definecolor{ma@green}{HTML}{004F00}
 
+\newcommand*\ma@punct{ma@green}
 \newcommand*\ma@fwd{ma@black}
 \newcommand*\ma@open{ma@blue}
 \newcommand*\ma@exit{ma@blue}
 \newcommand*\ma@prim{ma@purple}
 \newcommand*\ma@qed{ma@blue}
 
-\newcommand*\neverindent{\setlength\parindent{0pt}}
+\newcommand*\ma@constr[1]{{\color{\ma@punct}#1}}
+\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
+
+\newcommand*\ma@cast{\mathbin\ma@constr{:}}
+\newcommand*\ma@abbr{\mathrel\ma@constr{\eqdef}}
+\newcommand*\ma@prod{\mathord\ma@constr{\Pi}}
+\newcommand*\ma@arrw{\mathrel\ma@constr{\Rightarrow}}
+\newcommand*\ma@fall{\mathord\ma@constr{\forall}}
+\newcommand*\ma@impl{\mathrel\ma@constr{\supset}}
+\newcommand*\ma@case{\mathrel\ma@constr{\questeq}}
+\newcommand*\ma@caze{\mathrel\ma@constr{\mapsto}}
+\newcommand*\ma@pair{\mathbin\ma@constr{\mapsto}}
+\newcommand*\ma@cm{\ma@thop{\ma@constr{,}}}
+\newcommand*\ma@or{\mathbin\ma@constr{\vert}}
+\newcommand*\ma@op{\mathopen\ma@constr{(}}
+\newcommand*\ma@cp{\mathclose\ma@constr{)}\allowbreak}
+\newcommand*\ma@qm{\mathord\ma@constr{?}}
 
 %\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
 %\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
@@ -54,14 +64,18 @@
 \newcommand*\ObjIncNode{}
 \newcommand*\ObjNode{}
 
-\newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
-\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
-
-\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par}
-\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par}
-\newenvironment{definition}[2]{$}{$\par}
-\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par}
-\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
+\newcommand*\ma@thehead[4]{\ObjIncNode
+   \textbf{#1 \ObjNode:} (\ma@settarget{#3}{#4}) \textit{#2:}%
+   \neverindent\par
+}
+\newcommand*\ma@theneck[1]{\textit{#1:}\neverindent\par}
+
+\newenvironment{assumption}[2]{\ma@thehead{Assumption}{has type}{#1}{#2}$}{$\par}
+\newenvironment{axiom}[2]{\ma@thehead{Axiom}{states}{#1}{#2}$}{$\par}
+\newenvironment{declaration}[2]{\ma@thehead{Definition}{of type}{#1}{#2}$}{$\par}
+\newenvironment{definition}[2]{\ma@theneck{is defined as}$}{$\par}
+\newenvironment{proposition}[2]{\ma@thehead{Proposition}{stating}{#1}{#2}$}{$\par}
+\newenvironment{proof}[2]{\ma@theneck{is proved by}}{\par}
 \newenvironment{ma@step}[1]{\color{#1}}{\par}
 
 \newcommand*\ma@tmp{}
@@ -70,13 +84,8 @@
    \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi
    \ma@tmp{#3}{#2}{#3}{#4}%
 }
-\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
-\newcommand*\ma@cm{\ma@thop{,}}
-\newcommand*\ma@or{\mathbin\vert}
-\newcommand*\ma@cp{)\allowbreak}
-\newcommand*\ma@qm{\mathord{?}}
 \newcommand*\ma@arg[1]{#1}
-\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp}
+\newcommand*\ma@args{\ma@op\ma@list\relax\ma@arg\ma@cm\ma@cp}
 \newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax}
 \newcommand*\ma@bind{\ma@thop{}}
 \newcommand*\ma@skip[1]{}
@@ -86,19 +95,19 @@
 \newcommand*\TYPE[1]{\mathord\mathrm{TYPE}}
 \newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}}
 \newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}}
-\newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind}
-\newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind}
+\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\ABST[3]{\ma@op\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind}
 \newcommand*\PROD[3]{\def\ma@tmp{#2}%
    \ifx\ma@tmp\empty #3\ma@arrw\else
-   (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
+   \ma@op\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
 }
 \newcommand*\FALL[3]{\def\ma@tmp{#2}%
    \ifx\ma@tmp\empty #3\ma@impl\else
-   (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
+   \ma@op\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
 }
 \newcommand*\APPL[1]{#1\ma@args}
 \newcommand*\CASE[3]{#3\ma@case\ma@cases}
-\newcommand*\CAZE[3]{#3\ma@caze(\ma@qm\ma@cast #2)\ma@cases}
+\newcommand*\CAZE[3]{#3\ma@caze\ma@op\ma@qm\ma@cast #2\ma@cp\ma@cases}
 \newcommand*\PAIR[2]{#1\ma@pair #2}
 
 \newcommand*\ma@term[1]{$#1$}

diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index 0cf2e639fe774755dec155cb79b8b51bba482a43..a1591d4d54fb8e2fdf6a080f4d78b76e5cf7f706 100644 (file)
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -10,7 +10,7 @@
 
 \newcounter{node}
 \renewcommand*\ObjIncNode{\stepcounter{node}}
-\renewcommand*\ObjNode{\arabic{node} }
+\renewcommand*\ObjNode{\arabic{node}}
 
 \title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$:
 Definitions and Statements}