equal
deleted
inserted
replaced
3 (** bootstrap phase 0: towards secure ML barrier *) |
3 (** bootstrap phase 0: towards secure ML barrier *) |
4 |
4 |
5 structure Distribution = (*filled-in by makedist*) |
5 structure Distribution = (*filled-in by makedist*) |
6 struct |
6 struct |
7 val version = "unidentified repository version"; |
7 val version = "unidentified repository version"; |
|
8 val is_identified = false; |
8 val is_official = false; |
9 val is_official = false; |
9 end; |
10 end; |
10 |
11 |
11 |
12 |
12 (* library of general tools *) |
13 (* library of general tools *) |