]> matita.cs.unibo.it Git - helm.git/blob - provacoqcontribOmega.v
04d29942319cf7a0ff61fe4fa045f52fd209e307
[helm.git] / provacoqcontribOmega.v
1 Require Export Xml.
2
3 Require Omega.
4 Require Zlogarithm.
5 Require OmegaSyntax.
6 Require Zpower.
7
8 Print XML Module Disk "examples" Omega.
9 Print XML Module Disk "examples" Zlogarithm.
10 Print XML Module Disk "examples" OmegaSyntax.
11 Print XML Module Disk "examples" Zpower.