]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqcontribRing.v
update in ground_2 and basic_2
[helm.git] / helm / EXPORT / exportcoq / provacoqcontribRing.v
1 Require Export Xml.
2
3 Require ArithRing.
4 Require Quote.
5 Require Ring.
6 Require Ring_abstract.
7 Require Ring_normalize.
8 Require Ring_theory.
9 Require ZArithRing.
10
11 Print XML Module Disk "examples" ArithRing.
12 Print XML Module Disk "examples" Quote.
13 Print XML Module Disk "examples" Ring.
14 Print XML Module Disk "examples" Ring_abstract.
15 Print XML Module Disk "examples" Ring_normalize.
16 Print XML Module Disk "examples" Ring_theory.
17 Print XML Module Disk "examples" ZArithRing.