Generate SML module opens for dependent modules

[michaelsproul]

Holmake analyses the open statements in Script.sml files in order to work out the order that it should build files. Annoyingly, if you fail to specify a dependency in this way, Holmake will try and build the dependency in parallel with the module, which of course fails.

Instead it might be nice to generate an open which contains all the dependent theories like:

(* Unbaked *)
require a b c;

(* Baked *)
open aTheory bTheory cTheory;
val _ = translation_extends "c";

[michaelsproul]

Johannes suggested a clever fix for this, which is to combine the act of defining a module, with the act of declaring its dependencies, so something like:

package sysinit requires utils;

which expands to:

open utilsTheory;
val _ = new_theory "sysinit";
val _ = translation_extends "utils";

The rename from module -> package also seems like a good idea, given that module is already overloaded to mean SML-level module and CakeML-level module.

[LukeMondy]

This sounds good (this is also a test comment).