Summary
- merged
- more flexible syntax for theory load commands via Isabelle/Scala;
- clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;
- proper structural equality;
- more explicit types;
- unused (see 7634d33c1a79);
- clarified signature;
- clarified modules;
- clarified file names;
- tuned signature;
- refined syntax for bundle mixins for locale and class specifications