]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/provaStruct.v
bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
[helm.git] / helm / EXPORT / exportprove / provaStruct.v
1 Require Export Xml.
2
3 Require provastruct.
4 Print XML Module Disk "examples" provastruct.
5
6 Require provastruct2.
7 Print XML Module Disk "examples" provastruct2.
8
9 Require provastruct3.
10 Print XML Module Disk "examples" provastruct3.
11
12 Require provastruct4.
13 Print XML Module Disk "examples" provastruct4.
14
15 Require provastruct5.
16 Print XML Module Disk "examples" provastruct5.