]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqRelations.v
...
[helm.git] / helm / EXPORT / exportcoq / provacoqRelations.v
1 Require Export Xml.
2
3 Require Newman.
4 Require Operators_Properties.
5 Require Relation_Definitions.
6 Require Relation_Operators.
7 Require Relations.
8 Require Rstar.
9 (*Require Disjoint_Union.*)
10 (*Require Inclusion.*)
11 (*Require Inverse_Image.*)
12 (*Require Lexicographic_Exponentiation.*)
13 (*Require Lexicographic_Product.*)
14 (*Require Transitive_Closure.*)
15 (*Require Union.*)
16 (*Require Well_Ordering.*)
17 (*Require Wellfounded.*)
18
19 Print XML Module Disk "examples" Newman.
20 Print XML Module Disk "examples" Operators_Properties.
21 Print XML Module Disk "examples" Relation_Definitions.
22 Print XML Module Disk "examples" Relation_Operators.
23 Print XML Module Disk "examples" Relations.
24 Print XML Module Disk "examples" Rstar.
25 (*Print XML Module Disk "examples/WELLFOUNDED" Disjoint_Union.*)
26 (*Print XML Module Disk "examples/WELLFOUNDED" Inclusion.*)
27 (*Print XML Module Disk "examples/WELLFOUNDED" Inverse_Image.*)
28 (*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Exponentiation.*)
29 (*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Product.*)
30 (*Print XML Module Disk "examples/WELLFOUNDED" Transitive_Closure.*)
31 (*Print XML Module Disk "examples/WELLFOUNDED" Union.*)
32 (*Print XML Module Disk "examples/WELLFOUNDED" Well_Ordering.*)
33 (*Print XML Module Disk "examples/WELLFOUNDED" Wellfounded.*)