src/Pure/ROOT
author wenzelm
Tue, 01 Mar 2016 19:42:59 +0100
changeset 62490 39d01eaf5292
parent 62468 d97e13e5ea5b
child 62493 dd154240a53c
permissions -rw-r--r--
ML debugger support in Pure (again, see 3565c9f407ec);

chapter Pure

session RAW =
  theories
  files
    "RAW/ROOT_polyml-5.6.ML"
    "RAW/ROOT_polyml.ML"
    "RAW/compiler_polyml.ML"
    "RAW/exn.ML"
    "RAW/exn_trace.ML"
    "RAW/exn_trace_raw.ML"
    "RAW/fixed_int_dummy.ML"
    "RAW/ml_compiler_parameters.ML"
    "RAW/ml_compiler_parameters_polyml-5.6.ML"
    "RAW/ml_debugger.ML"
    "RAW/ml_debugger_polyml-5.6.ML"
    "RAW/ml_heap.ML"
    "RAW/ml_heap_polyml-5.3.0.ML"
    "RAW/ml_name_space_polyml-5.6.ML"
    "RAW/ml_name_space_polyml.ML"
    "RAW/ml_parse_tree.ML"
    "RAW/ml_parse_tree_polyml-5.6.ML"
    "RAW/ml_positions.ML"
    "RAW/ml_pretty.ML"
    "RAW/ml_profiling_polyml-5.6.ML"
    "RAW/ml_profiling_polyml.ML"
    "RAW/ml_stack_dummy.ML"
    "RAW/ml_stack_polyml-5.6.ML"
    "RAW/ml_system.ML"
    "RAW/multithreading.ML"
    "RAW/single_assignment_polyml.ML"
    "RAW/unsynchronized.ML"

session Pure =
  global_theories Pure
  files
    "RAW/ROOT_polyml-5.6.ML"
    "RAW/ROOT_polyml.ML"
    "RAW/compiler_polyml.ML"
    "RAW/exn.ML"
    "RAW/exn_trace.ML"
    "RAW/exn_trace_raw.ML"
    "RAW/fixed_int_dummy.ML"
    "RAW/ml_compiler_parameters.ML"
    "RAW/ml_compiler_parameters_polyml-5.6.ML"
    "RAW/ml_debugger.ML"
    "RAW/ml_debugger_polyml-5.6.ML"
    "RAW/ml_heap.ML"
    "RAW/ml_heap_polyml-5.3.0.ML"
    "RAW/ml_name_space_polyml-5.6.ML"
    "RAW/ml_name_space_polyml.ML"
    "RAW/ml_parse_tree.ML"
    "RAW/ml_parse_tree_polyml-5.6.ML"
    "RAW/ml_positions.ML"
    "RAW/ml_pretty.ML"
    "RAW/ml_profiling_polyml-5.6.ML"
    "RAW/ml_profiling_polyml.ML"
    "RAW/ml_stack_dummy.ML"
    "RAW/ml_stack_polyml-5.6.ML"
    "RAW/ml_system.ML"
    "RAW/multithreading.ML"
    "RAW/single_assignment_polyml.ML"
    "RAW/unsynchronized.ML"

    "Concurrent/bash.ML"
    "Concurrent/bash_windows.ML"
    "Concurrent/cache.ML"
    "Concurrent/counter.ML"
    "Concurrent/event_timer.ML"
    "Concurrent/future.ML"
    "Concurrent/lazy.ML"
    "Concurrent/mailbox.ML"
    "Concurrent/par_exn.ML"
    "Concurrent/par_list.ML"
    "Concurrent/random.ML"
    "Concurrent/single_assignment.ML"
    "Concurrent/standard_thread.ML"
    "Concurrent/synchronized.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/input.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/experiment.ML"
    "Isar/expression.ML"
    "Isar/generic_target.ML"
    "Isar/interpretation.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/subgoal.ML"
    "Isar/token.ML"
    "Isar/toplevel.ML"
    "Isar/typedecl.ML"
    "ML/exn_output.ML"
    "ML/exn_properties.ML"
    "ML/install_pp_polyml.ML"
    "ML/ml_antiquotation.ML"
    "ML/ml_compiler.ML"
    "ML/ml_context.ML"
    "ML/ml_env.ML"
    "ML/ml_file.ML"
    "ML/ml_lex.ML"
    "ML/ml_options.ML"
    "ML/ml_parse.ML"
    "ML/ml_statistics.ML"
    "ML/ml_statistics_dummy.ML"
    "ML/ml_syntax.ML"
    "PIDE/active.ML"
    "PIDE/command.ML"
    "PIDE/command_span.ML"
    "PIDE/document.ML"
    "PIDE/document_id.ML"
    "PIDE/execution.ML"
    "PIDE/markup.ML"
    "PIDE/protocol.ML"
    "PIDE/protocol_message.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/message_channel.ML"
    "System/options.ML"
    "System/system_channel.ML"
    "Thy/document_antiquotations.ML"
    "Thy/html.ML"
    "Thy/latex.ML"
    "Thy/markdown.ML"
    "Thy/present.ML"
    "Thy/term_style.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/plugin.ML"
    "assumption.ML"
    "axclass.ML"
    "config.ML"
    "conjunction.ML"
    "consts.ML"
    "context.ML"
    "context_position.ML"
    "conv.ML"
    "defs.ML"
    "drule.ML"
    "envir.ML"
    "facts.ML"
    "global_theory.ML"
    "goal.ML"
    "goal_display.ML"
    "item_net.ML"
    "library.ML"
    "logic.ML"
    "more_pattern.ML"
    "more_thm.ML"
    "more_unify.ML"
    "morphism.ML"
    "name.ML"
    "net.ML"
    "par_tactical.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"
    "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"