X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk_gtkmathview%2Flablgtk-20000829_gtkmathview-0.2.0%2Fminidom%2Ftest.xml;h=83d2eef68bbdf76d2246b7993d56678810452f8d;hb=e8aaa9c3fe3d2af0c863261b3c06f66b72923c89;hp=bdac517a30368dd310f899bd08f2293384685e32;hpb=baffca1ac75af466a7b5cf2c1513a0f1ec4a8000;p=helm.git diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml index bdac517a3..83d2eef68 100644 --- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml +++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml @@ -1,3 +1,505 @@ - - - + + + + + + + + DEFINITION and_ind() OF TYPE + + + + + + + + __ + + + + + + + + ( + + + + + Π + A + : + + Prop + + + + + + + . + + + + + Π + B + : + + Prop + + + + + + + . + + + + + Π + P + : + + Prop + + + + + + + . + + + + + Π + f + : + + ( + A + + + ( + B + + P + ) + + ) + + + + + + + . + + Π + a + : + + ( + and + + _ + + A + + _ + + B + ) + + . + P + + + + + + + + + + + + + + + + + + + + + + + + + + + + :> + + Prop + + + + + + + + ) + + + + + + + + cast + + prod + + A + + + Prop + + + + + prod + + B + + + Prop + + + + + prod + + P + + + Prop + + + + + prod + + f + + + arrow + A + + arrow + B + P + + + + + + prod + + a + + + app + and + A + B + + + + P + + + + + + + Prop + + + + + + + + + + + AS + + + + + + + + __ + + + + + + + λ + A + : + + Prop + + + + + + + . + + + + + λ + B + : + + Prop + + + + + + + . + + + + + λ + P + : + + Prop + + + + + + + . + + + + + λ + f + : + + ( + A + + + ( + B + + P + ) + + ) + + + + + + + . + + + + + λ + a + : + + ( + and + + _ + + A + + _ + + B + ) + + + + + + + . + + < + P + > + CASES + + _ + + a + + _ + + OF + + ( + conj + + _ + + $1 + + _ + + $2 + ) + + + + ( + f + + _ + + $1 + + _ + + $2 + ) + + + _ + + END + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + A + + + Prop + + + + + + B + + + Prop + + + + + + P + + + Prop + + + + + + f + + + arrow + A + + arrow + B + P + + + + + + + a + + + app + and + A + B + + + + + mutcase + P + a + + app + conj + $1 + $2 + + + app + f + $1 + $2 + + + + + + + + + + + + + +