(*specifications*)

 (*specifications*)

 use "Isar/parse_spec.ML";

 use "Isar/parse_spec.ML";

 use "Isar/spec_rules.ML";

 use "Isar/spec_rules.ML";

 use "Isar/specification.ML";

 use "Isar/specification.ML";

 use "Isar/typedecl.ML";

 use "Isar/typedecl.ML";

 (*toplevel transactions*)

 (*toplevel transactions*)

 use "Thy/thy_load.ML";

 use "Thy/thy_load.ML";

 use "Isar/proof_node.ML";

 use "Isar/proof_node.ML";

 use "Isar/toplevel.ML";

 use "Isar/toplevel.ML";