clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
chapter Pure
session RAW =
theories
files
"General/exn.ML"
"ML-Systems/compiler_polyml.ML"
"ML-Systems/ml_name_space.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
"ML-Systems/multithreading_polyml.ML"
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
"ML-Systems/single_assignment.ML"
"ML-Systems/single_assignment_polyml.ML"
"ML-Systems/share_common_data_polyml-5.3.0.ML"
"ML-Systems/smlnj.ML"
"ML-Systems/thread_dummy.ML"
"ML-Systems/universal.ML"
"ML-Systems/unsynchronized.ML"
"ML-Systems/use_context.ML"
session Pure =
theories Pure
files
"General/exn.ML"
"ML-Systems/compiler_polyml.ML"
"ML-Systems/ml_name_space.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
"ML-Systems/multithreading_polyml.ML"
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
"ML-Systems/single_assignment.ML"
"ML-Systems/single_assignment_polyml.ML"
"ML-Systems/smlnj.ML"
"ML-Systems/thread_dummy.ML"
"ML-Systems/universal.ML"
"ML-Systems/unsynchronized.ML"
"ML-Systems/use_context.ML"
"Concurrent/bash.ML"
"Concurrent/bash_sequential.ML"
"Concurrent/cache.ML"
"Concurrent/event_timer.ML"
"Concurrent/future.ML"
"Concurrent/lazy.ML"
"Concurrent/lazy_sequential.ML"
"Concurrent/mailbox.ML"
"Concurrent/par_exn.ML"
"Concurrent/par_list.ML"
"Concurrent/par_list_sequential.ML"
"Concurrent/simple_thread.ML"
"Concurrent/single_assignment.ML"
"Concurrent/single_assignment_sequential.ML"
"Concurrent/synchronized.ML"
"Concurrent/synchronized_sequential.ML"
"Concurrent/task_queue.ML"
"Concurrent/time_limit.ML"
"General/alist.ML"
"General/antiquote.ML"
"General/balanced_tree.ML"
"General/basics.ML"
"General/binding.ML"
"General/buffer.ML"
"General/change_table.ML"
"General/completion.ML"
"General/file.ML"
"General/graph.ML"
"General/graph_display.ML"
"General/heap.ML"
"General/integer.ML"
"General/linear_set.ML"
"General/long_name.ML"
"General/name_space.ML"
"General/ord_list.ML"
"General/output.ML"
"General/path.ML"
"General/position.ML"
"General/pretty.ML"
"General/print_mode.ML"
"General/properties.ML"
"General/queue.ML"
"General/same.ML"
"General/scan.ML"
"General/secure.ML"
"General/seq.ML"
"General/sha1.ML"
"General/sha1_polyml.ML"
"General/sha1_samples.ML"
"General/socket_io.ML"
"General/source.ML"
"General/stack.ML"
"General/symbol.ML"
"General/symbol_pos.ML"
"General/table.ML"
"General/timing.ML"
"General/url.ML"
"Isar/args.ML"
"Isar/attrib.ML"
"Isar/auto_bind.ML"
"Isar/bundle.ML"
"Isar/class.ML"
"Isar/class_declaration.ML"
"Isar/code.ML"
"Isar/context_rules.ML"
"Isar/element.ML"
"Isar/expression.ML"
"Isar/generic_target.ML"
"Isar/isar_cmd.ML"
"Isar/keyword.ML"
"Isar/local_defs.ML"
"Isar/local_theory.ML"
"Isar/locale.ML"
"Isar/method.ML"
"Isar/named_target.ML"
"Isar/object_logic.ML"
"Isar/obtain.ML"
"Isar/outer_syntax.ML"
"Isar/overloading.ML"
"Isar/parse.ML"
"Isar/parse_spec.ML"
"Isar/proof.ML"
"Isar/proof_context.ML"
"Isar/proof_display.ML"
"Isar/proof_node.ML"
"Isar/rule_cases.ML"
"Isar/runtime.ML"
"Isar/spec_rules.ML"
"Isar/specification.ML"
"Isar/token.ML"
"Isar/toplevel.ML"
"Isar/typedecl.ML"
"ML/exn_output.ML"
"ML/exn_output_polyml.ML"
"ML/exn_properties_dummy.ML"
"ML/exn_properties_polyml.ML"
"ML/exn_trace_polyml-5.5.1.ML"
"ML/install_pp_polyml.ML"
"ML/ml_antiquotation.ML"
"ML/ml_compiler.ML"
"ML/ml_compiler_polyml.ML"
"ML/ml_context.ML"
"ML/ml_env.ML"
"ML/ml_lex.ML"
"ML/ml_parse.ML"
"ML/ml_options.ML"
"ML/ml_statistics_dummy.ML"
"ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
"PIDE/active.ML"
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/document_id.ML"
"PIDE/execution.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/query_operation.ML"
"PIDE/resources.ML"
"PIDE/session.ML"
"PIDE/xml.ML"
"PIDE/yxml.ML"
"Proof/extraction.ML"
"Proof/proof_checker.ML"
"Proof/proof_rewrite_rules.ML"
"Proof/proof_syntax.ML"
"Proof/reconstruct.ML"
"ROOT.ML"
"Syntax/ast.ML"
"Syntax/lexicon.ML"
"Syntax/local_syntax.ML"
"Syntax/mixfix.ML"
"Syntax/parser.ML"
"Syntax/printer.ML"
"Syntax/simple_syntax.ML"
"Syntax/syntax.ML"
"Syntax/syntax_ext.ML"
"Syntax/syntax_phases.ML"
"Syntax/syntax_trans.ML"
"Syntax/term_position.ML"
"Syntax/type_annotation.ML"
"System/command_line.ML"
"System/invoke_scala.ML"
"System/isabelle_process.ML"
"System/isabelle_system.ML"
"System/isar.ML"
"System/message_channel.ML"
"System/options.ML"
"System/system_channel.ML"
"Thy/html.ML"
"Thy/latex.ML"
"Thy/present.ML"
"Thy/term_style.ML"
"Thy/thm_deps.ML"
"Thy/thy_header.ML"
"Thy/thy_info.ML"
"Thy/thy_output.ML"
"Thy/thy_syntax.ML"
"Tools/build.ML"
"Tools/named_thms.ML"
"Tools/proof_general.ML"
"assumption.ML"
"axclass.ML"
"config.ML"
"conjunction.ML"
"consts.ML"
"context.ML"
"context_position.ML"
"conv.ML"
"defs.ML"
"display.ML"
"drule.ML"
"envir.ML"
"facts.ML"
"global_theory.ML"
"goal.ML"
"goal_display.ML"
"interpretation.ML"
"item_net.ML"
"library.ML"
"logic.ML"
"more_thm.ML"
"morphism.ML"
"name.ML"
"net.ML"
"pattern.ML"
"primitive_defs.ML"
"proofterm.ML"
"pure_syn.ML"
"pure_thy.ML"
"raw_simplifier.ML"
"search.ML"
"sign.ML"
"simplifier.ML"
"skip_proof.ML"
"sorts.ML"
"subgoal.ML"
"tactic.ML"
"tactical.ML"
"term.ML"
"term_ord.ML"
"term_sharing.ML"
"term_subst.ML"
"term_xml.ML"
"theory.ML"
"thm.ML"
"type.ML"
"type_infer.ML"
"type_infer_context.ML"
"unify.ML"
"variable.ML"