]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the...
[helm.git] / helm / EXPORT / export_Rocq_SHUFFLE / prova_Rocq_SHUFFLE.v
1 Require Export Xml.
2
3 Require Alternate.
4 Require Gilbreath.
5 Require Opposite.
6 Require Paired.
7 Require Shuffle.
8 Require Words.
9
10
11 Print XML Module Disk "examples" Alternate.
12 Print XML Module Disk "examples" Gilbreath.
13 Print XML Module Disk "examples" Opposite.
14 Print XML Module Disk "examples" Paired.
15 Print XML Module Disk "examples" Shuffle.
16 Print XML Module Disk "examples" Words.