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=1f4c7bf28fbaf6b0d2f5979c5ed89912f9818dff;hp=bdac517a30368dd310f899bd08f2293384685e32;hpb=81214a3e858c8a883785e7b5df51bb79eba244e1;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
+
+
+
+
+
+
+
+
+
+
+
+
+
+