]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqLists.v
Added aliases and notation.
[helm.git] / helm / EXPORT / exportcoq / provacoqLists.v
1 Require Export Xml.
2
3 Require List.
4 Require ListSet.
5 Require PolyList.
6 (*Require PolyListSyntax.*)
7 Require Streams.
8 Require TheoryList.
9
10 Print XML Module Disk "examples" List.
11 Print XML Module Disk "examples" ListSet.
12 Print XML Module Disk "examples" PolyList.
13 (*Print XML Module Disk "examples" PolyListSyntax.*)
14 Print XML Module Disk "examples" Streams.
15 Print XML Module Disk "examples" TheoryList.