]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqSets.v
All the equalityTactics have now been ported to use both the equality of
[helm.git] / helm / EXPORT / exportcoq / provacoqSets.v
1 Require Export Xml.
2
3 Require Classical_sets.
4 Require Constructive_sets.
5 Require Cpo.
6 Require Ensembles.
7 Require Finite_sets.
8 Require Finite_sets_facts.
9 Require Image.
10 Require Infinite_sets.
11 Require Integers.
12 Require Multiset.
13 Require Partial_Order.
14 Require Permut.
15 (*Require CSCPermut.*)
16 Require Powerset.
17 Require Powerset_Classical_facts.
18 Require Powerset_facts.
19 Require Relations_1.
20 Require Relations_1_facts.
21 Require Relations_2.
22 Require Relations_2_facts.
23 Require Relations_3.
24 Require Relations_3_facts.
25 Require Uniset.
26
27 Print XML Module Disk "examples" Classical_sets.
28 Print XML Module Disk "examples" Constructive_sets.
29 Print XML Module Disk "examples" Cpo.
30 Print XML Module Disk "examples" Ensembles.
31 Print XML Module Disk "examples" Finite_sets.
32 Print XML Module Disk "examples" Finite_sets_facts.
33 Print XML Module Disk "examples" Image.
34 Print XML Module Disk "examples" Infinite_sets.
35 Print XML Module Disk "examples" Integers.
36 Print XML Module Disk "examples" Multiset.
37 Print XML Module Disk "examples" Partial_Order.
38 Print XML Module Disk "examples" Permut.
39 Print XML Module Disk "examples" Powerset.
40 Print XML Module Disk "examples" Powerset_Classical_facts.
41 Print XML Module Disk "examples" Powerset_facts.
42 Print XML Module Disk "examples" Relations_1.
43 Print XML Module Disk "examples" Relations_1_facts.
44 Print XML Module Disk "examples" Relations_2.
45 Print XML Module Disk "examples" Relations_2_facts.
46 Print XML Module Disk "examples" Relations_3.
47 Print XML Module Disk "examples" Relations_3_facts.
48 Print XML Module Disk "examples" Uniset.